src/HOL/Tools/record.ML

         (Typedef.add_typedef overloaded (raw_tyco, vs, NoSyn)
           (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1))
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;
 
-fun mk_cons_tuple (left, right) =
-  let
-    val (leftT, rightT) = (fastype_of left, fastype_of right);
-    val prodT = HOLogic.mk_prodT (leftT, rightT);
-    val isomT = Type (\<^type_name>\<open>tuple_isomorphism\<close>, [prodT, leftT, rightT]);
-  in
-    Const (\<^const_name>\<open>Record.iso_tuple_cons\<close>, isomT --> leftT --> rightT --> prodT) $
-      Const (fst tuple_iso_tuple, isomT) $ left $ right
-  end;
-
-fun dest_cons_tuple (Const (\<^const_name>\<open>Record.iso_tuple_cons\<close>, _) $ Const _ $ t $ u) = (t, u)
+fun mk_cons_tuple (t, u) =
+  let val (A, B) = apply2 fastype_of (t, u)
+  in \<^Const>\<open>iso_tuple_cons \<^Type>\<open>prod A B\<close> A B for \<^Const>\<open>tuple_iso_tuple A B\<close> t u\<close> end;
+
+fun dest_cons_tuple \<^Const_>\<open>iso_tuple_cons _ _ _ for \<open>Const _\<close> t u\<close> = (t, u)
   | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
 
 fun add_iso_tuple_type overloaded (b, alphas) (leftT, rightT) thy =
   let
     val repT = HOLogic.mk_prodT (leftT, rightT);

       |> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd
       |> Global_Theory.add_defs false
         [((Binding.concealed (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
 
     val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
-    val cons = Const (\<^const_name>\<open>Record.iso_tuple_cons\<close>, isomT --> leftT --> rightT --> absT);
+    val cons = \<^Const>\<open>iso_tuple_cons absT leftT rightT\<close>;
 
     val thm_thy =
       cdef_thy
       |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
       |> Sign.restore_naming thy

       fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);
 
       val goal' = Envir.beta_eta_contract goal;
       val is =
         (case goal' of
-          Const (\<^const_name>\<open>Trueprop\<close>, _) $
-            (Const (\<^const_name>\<open>isomorphic_tuple\<close>, _) $ Const is) => is
+          \<^Const_>\<open>Trueprop for \<^Const>\<open>isomorphic_tuple _ _ _ for \<open>Const is\<close>\<close>\<close> => is
         | _ => err "unexpected goal format" goal');
       val isthm =
         (case Symtab.lookup isthms (#1 is) of
           SOME isthm => isthm
         | NONE => err "no thm found for constant" (Const is));

     SOME u_name => u_name = s
   | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
 
 fun mk_comp_id f =
   let val T = range_type (fastype_of f)
-  in HOLogic.mk_comp (Const (\<^const_name>\<open>Fun.id\<close>, T --> T), f) end;
+  in HOLogic.mk_comp (\<^Const>\<open>id T\<close>, f) end;
 
 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
   | get_upd_funs _ = [];
 
 fun get_accupd_simps ctxt term defset =

 val eq_simproc =
   Simplifier.make_simproc \<^context> "record_eq"
    {lhss = [\<^term>\<open>r = s\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of
-        Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) $ _ $ _ =>
+        \<^Const_>\<open>HOL.eq T for _ _\<close> =>
           (case rec_id ~1 T of
             "" => NONE
           | name =>
               (case get_equalities (Proof_Context.theory_of ctxt) name of
                 NONE => NONE

    {lhss = [\<^term>\<open>Ex t\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
         val t = Thm.term_of ct;
-        fun mkeq (lr, Teq, (sel, Tsel), x) i =
+        fun mkeq (lr, T, (sel, Tsel), x) i =
           if is_selector thy sel then
             let
               val x' =
                 if not (Term.is_dependent x)
                 then Free ("x" ^ string_of_int i, range_type Tsel)
                 else raise TERM ("", [x]);
               val sel' = Const (sel, Tsel) $ Bound 0;
               val (l, r) = if lr then (sel', x') else (x', sel');
-            in Const (\<^const_name>\<open>HOL.eq\<close>, Teq) $ l $ r end
+            in \<^Const>\<open>HOL.eq T for l r\<close> end
           else raise TERM ("", [Const (sel, Tsel)]);
 
-        fun dest_sel_eq (Const (\<^const_name>\<open>HOL.eq\<close>, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
-              (true, Teq, (sel, Tsel), X)
-          | dest_sel_eq (Const (\<^const_name>\<open>HOL.eq\<close>, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
-              (false, Teq, (sel, Tsel), X)
+        fun dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ (Const (sel, Tsel) $ Bound 0) $ X) =
+              (true, T, (sel, Tsel), X)
+          | dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ X $ (Const (sel, Tsel) $ Bound 0)) =
+              (false, T, (sel, Tsel), X)
           | dest_sel_eq _ = raise TERM ("", []);
       in
         (case t of
-          Const (\<^const_name>\<open>Ex\<close>, Tex) $ Abs (s, T, t) =>
+          \<^Const_>\<open>Ex T for \<open>Abs (s, _, t)\<close>\<close> =>
            (let
              val eq = mkeq (dest_sel_eq t) 0;
              val prop =
                Logic.list_all ([("r", T)],
-                 Logic.mk_equals
-                  (Const (\<^const_name>\<open>Ex\<close>, Tex) $ Abs (s, T, eq), \<^term>\<open>True\<close>));
+                 Logic.mk_equals (\<^Const>\<open>Ex T for \<open>Abs (s, T, eq)\<close>\<close>, \<^Const>\<open>True\<close>));
             in
               SOME (Goal.prove_sorry_global thy [] [] prop
                 (fn {context = ctxt', ...} =>
                   simp_tac (put_simpset (get_simpset thy) ctxt'
                     addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))

     val size = \<^term>\<open>i::natural\<close>;
     fun termifyT T = HOLogic.mk_prodT (T, \<^typ>\<open>unit \<Rightarrow> term\<close>);
     val T = Type (tyco, map TFree vs);
     val test_function = Free ("f", termifyT T --> \<^typ>\<open>(bool \<times> term list) option\<close>);
     val params = Name.invent_names Name.context "x" Ts;
-    fun full_exhaustiveT T =
-      (termifyT T --> \<^typ>\<open>(bool \<times> Code_Evaluation.term list) option\<close>) -->
-        \<^typ>\<open>natural\<close> --> \<^typ>\<open>(bool \<times> Code_Evaluation.term list) option\<close>;
-    fun mk_full_exhaustive T =
-      Const (\<^const_name>\<open>Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive\<close>,
-        full_exhaustiveT T);
+    fun mk_full_exhaustive U = \<^Const>\<open>full_exhaustive_class.full_exhaustive U\<close>;
     val lhs = mk_full_exhaustive T $ test_function $ size;
     val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
-    val rhs = fold_rev (fn (v, T) => fn cont =>
-        mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
+    val rhs = fold_rev (fn (v, U) => fn cont =>
+        mk_full_exhaustive U $ (lambda (Free (v, termifyT U)) cont) $ size) params tc;
   in
     (lhs, rhs)
   end;
 
 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =

   end;
 
 fun add_code ext_tyco vs extT ext simps inject thy =
   if Config.get_global thy codegen then
     let
-      val eq =
-        HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (Const (\<^const_name>\<open>HOL.equal\<close>, extT --> extT --> HOLogic.boolT),
-           Const (\<^const_name>\<open>HOL.eq\<close>, extT --> extT --> HOLogic.boolT)));
+      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (\<^Const>\<open>HOL.equal extT\<close>, \<^Const>\<open>HOL.eq extT\<close>));
       fun tac ctxt eq_def =
         Class.intro_classes_tac ctxt []
         THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]
         THEN ALLGOALS (resolve_tac ctxt @{thms refl});
       fun mk_eq ctxt eq_def =