tuned;
authorwenzelm
Sun, 21 Jul 2019 12:28:02 +0200
changeset 70572 35dd9212bf29
parent 70571 6af87375b95f
child 70573 e31271559de8
tuned;
src/HOL/Tools/SMT/smt_builtin.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/object_logic.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/axclass.ML
src/Tools/Code/code_runtime.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Sun Jul 21 12:11:35 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Sun Jul 21 12:28:02 2019 +0200
@@ -180,7 +180,7 @@
 
 fun dest_builtin_eq ctxt t u =
   let
-    val aT = TFree (Name.aT, \<^sort>\<open>type\<close>)
+    val aT = Term.aT \<^sort>\<open>type\<close>
     val c = (\<^const_name>\<open>HOL.eq\<close>, aT --> aT --> \<^typ>\<open>bool\<close>)
     fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts)
   in
--- a/src/Pure/Isar/class.ML	Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Pure/Isar/class.ML	Sun Jul 21 12:28:02 2019 +0200
@@ -309,7 +309,7 @@
               (case Vartab.lookup tyenv (Name.aT, 0) of
                 SOME (_, ty' as TVar (vi, sort)) =>
                   if Type_Infer.is_param vi andalso Sorts.sort_le algebra (base_sort, sort)
-                  then SOME (ty', TFree (Name.aT, base_sort))
+                  then SOME (ty', Term.aT base_sort)
                   else NONE
               | _ => NONE)
           | NONE => NONE)
@@ -335,8 +335,7 @@
 
 fun begin sort base_sort ctxt =
   ctxt
-  |> Variable.declare_term
-      (Logic.mk_type (TFree (Name.aT, base_sort)))
+  |> Variable.declare_term (Logic.mk_type (Term.aT base_sort))
   |> synchronize_class_syntax sort base_sort
   |> Overloading.activate_improvable_syntax;
 
--- a/src/Pure/Isar/class_declaration.ML	Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Sun Jul 21 12:28:02 2019 +0200
@@ -41,7 +41,7 @@
     val const_morph =
       Element.instantiate_normalize_morphism ([], param_map_inst);
     val typ_morph =
-      Element.instantiate_normalize_morphism ([(a_tfree, certT (TFree (Name.aT, [class])))], [])
+      Element.instantiate_normalize_morphism ([(a_tfree, certT (Term.aT [class]))], [])
     val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = thy_ctxt
       |> Expression.cert_goal_expression ([(class, (("", false),
            (Expression.Named param_map_const, [])))], []);
@@ -139,7 +139,7 @@
                   " of type parameter " ^ Name.aT ^ " of sort " ^
                   Syntax.string_of_sort_global thy S)
           | _ => error "Multiple type variables in class specification");
-        val fixateT = TFree (Name.aT, fixate_sort);
+        val fixateT = Term.aT fixate_sort;
       in
         (map o map_atyps)
           (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts
@@ -194,7 +194,7 @@
         | [(_, sort)] => sort
         | _ => error "Multiple type variables in class specification");
     val supparams = map (fn ((c, T), _) =>
-      (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
+      (c, map_atyps (K (Term.aT base_sort)) T)) raw_supparams;
     val supparam_names = map fst supparams;
     fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c);
     val supexpr = (map (fn sup => (sup, (("", false),
@@ -264,16 +264,16 @@
     (*FIXME simplify*)
     val supconsts = supparam_names
       |> AList.make (snd o the o AList.lookup (op =) (Class.these_params thy sups))
-      |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
+      |> (map o apsnd o apsnd o map_atyps) (K (Term.aT [class]));
     val all_params = Locale.params_of thy class;
     val raw_params = (snd o chop (length supparam_names)) all_params;
     fun add_const ((raw_c, raw_ty), _) thy =
       let
         val b = Binding.name raw_c;
         val c = Sign.full_name thy b;
-        val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
+        val ty = map_atyps (K (Term.aT base_sort)) raw_ty;
         val ty0 = Type.strip_sorts ty;
-        val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
+        val ty' = map_atyps (K (Term.aT [class])) ty0;
         val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
       in
         thy
--- a/src/Pure/Isar/object_logic.ML	Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Pure/Isar/object_logic.ML	Sun Jul 21 12:28:02 2019 +0200
@@ -126,7 +126,7 @@
 fun fixed_judgment ctxt x =
   let  (*be robust wrt. low-level errors*)
     val c = judgment_name ctxt;
-    val aT = TFree (Name.aT, []);
+    val aT = Term.aT [];
     val T =
       the_default (aT --> propT) (Sign.const_type (Proof_Context.theory_of ctxt) c)
       |> Term.map_type_tvar (fn ((a, _), S) => TFree (a, S));
--- a/src/Pure/Proof/proof_syntax.ML	Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Jul 21 12:28:02 2019 +0200
@@ -28,7 +28,7 @@
 val paramT = Type ("param", []);
 val paramsT = Type ("params", []);
 val idtT = Type ("idt", []);
-val aT = TFree (Name.aT, []);
+val aT = Term.aT [];
 
 
 (** constants for theorems and axioms **)
--- a/src/Pure/axclass.ML	Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Pure/axclass.ML	Sun Jul 21 12:28:02 2019 +0200
@@ -512,7 +512,7 @@
           (case Term.add_tvarsT T [] of
             [((a, _), S)] => check_constraint (a, S)
           | _ => error ("Exactly one type variable expected in class parameter " ^ quote p));
-        val T' = Term.map_type_tvar (fn _ => TFree (Name.aT, [class])) T;
+        val T' = Term.map_type_tvar (K (Term.aT [class])) T;
       in (p, T') end);
 
 
--- a/src/Tools/Code/code_runtime.ML	Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Tools/Code/code_runtime.ML	Sun Jul 21 12:28:02 2019 +0200
@@ -542,8 +542,9 @@
     val position_index' = #position_index data + 1;
     fun generated_code' () =
       let
-        val evals = Abs ("eval", map snd computation_cTs' --->
-          TFree (Name.aT, []), list_comb (Bound 0, map Const computation_cTs'))
+        val evals =
+          Abs ("eval", map snd computation_cTs' ---> Term.aT [],
+            list_comb (Bound 0, map Const computation_cTs'))
           |> preprocess_term { ctxt = ctxt } ctxt
       in Code_Thingol.dynamic_value ctxt
         (K I) (runtime_code ctxt NONE [] named_consts' computation_Ts') evals