diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
index fa9abccbd33..ec7e26e1722 100644
--- a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
+++ b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
@@ -643,22 +643,40 @@ let (head_and_args :
         { FStar_Syntax_Syntax.hd = head; FStar_Syntax_Syntax.args = args;_}
         -> (head, args)
     | uu___ -> (t1, [])
-let rec (head_and_args_full :
+let rec (__head_and_args_full :
+  Prims.bool ->
+    FStar_Syntax_Syntax.term ->
+      (FStar_Syntax_Syntax.term * (FStar_Syntax_Syntax.term'
+        FStar_Syntax_Syntax.syntax * FStar_Syntax_Syntax.arg_qualifier
+        FStar_Pervasives_Native.option) Prims.list))
+  =
+  fun unmeta1 ->
+    fun t ->
+      let t1 = FStar_Syntax_Subst.compress t in
+      match t1.FStar_Syntax_Syntax.n with
+      | FStar_Syntax_Syntax.Tm_app
+          { FStar_Syntax_Syntax.hd = head; FStar_Syntax_Syntax.args = args;_}
+          ->
+          let uu___ = __head_and_args_full unmeta1 head in
+          (match uu___ with
+           | (head1, args') ->
+               (head1, (FStar_Compiler_List.op_At args' args)))
+      | FStar_Syntax_Syntax.Tm_meta
+          { FStar_Syntax_Syntax.tm2 = tm; FStar_Syntax_Syntax.meta = uu___;_}
+          when unmeta1 -> __head_and_args_full unmeta1 tm
+      | uu___ -> (t1, [])
+let (head_and_args_full :
   FStar_Syntax_Syntax.term ->
     (FStar_Syntax_Syntax.term * (FStar_Syntax_Syntax.term'
       FStar_Syntax_Syntax.syntax * FStar_Syntax_Syntax.arg_qualifier
       FStar_Pervasives_Native.option) Prims.list))
-  =
-  fun t ->
-    let t1 = FStar_Syntax_Subst.compress t in
-    match t1.FStar_Syntax_Syntax.n with
-    | FStar_Syntax_Syntax.Tm_app
-        { FStar_Syntax_Syntax.hd = head; FStar_Syntax_Syntax.args = args;_}
-        ->
-        let uu___ = head_and_args_full head in
-        (match uu___ with
-         | (head1, args') -> (head1, (FStar_Compiler_List.op_At args' args)))
-    | uu___ -> (t1, [])
+  = fun t -> __head_and_args_full false t
+let (head_and_args_full_unmeta :
+  FStar_Syntax_Syntax.term ->
+    (FStar_Syntax_Syntax.term * (FStar_Syntax_Syntax.term'
+      FStar_Syntax_Syntax.syntax * FStar_Syntax_Syntax.arg_qualifier
+      FStar_Pervasives_Native.option) Prims.list))
+  = fun t -> __head_and_args_full true t
 let rec (leftmost_head :
   FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) =
   fun t ->
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml
index 2c93cae52fd..2dd6a14bf19 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml
@@ -694,11 +694,13 @@ let (reduce_primops :
               (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.primops
           then (tm, false)
           else
-            (let uu___1 = FStar_Syntax_Util.head_and_args tm in
+            (let uu___1 = FStar_Syntax_Util.head_and_args_full tm in
              match uu___1 with
              | (head, args) ->
                  let uu___2 =
-                   let head1 = FStar_Syntax_Subst.compress head in
+                   let head1 =
+                     let uu___3 = FStar_Syntax_Util.unmeta head in
+                     FStar_Syntax_Subst.compress uu___3 in
                    match head1.FStar_Syntax_Syntax.n with
                    | FStar_Syntax_Syntax.Tm_uinst (fv, us) -> (fv, us)
                    | uu___3 -> (head1, []) in
@@ -6782,7 +6784,7 @@ and (do_rebuild :
                | FStar_Syntax_Syntax.Tm_app uu___1 when
                    (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.primops
                    ->
-                   let uu___2 = FStar_Syntax_Util.head_and_args t in
+                   let uu___2 = FStar_Syntax_Util.head_and_args_full_unmeta t in
                    (match uu___2 with
                     | (hd, args) ->
                         let uu___3 =