# HG changeset patch
# User wenzelm
# Date 1395508797 -3600
# Node ID a2dd9200854dcb28be7b04e14352021850d16a2b
# Parent  83b3c110f22d61a14419ad04817af58cafc857f5
more antiquotations;

diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -434,7 +434,7 @@
 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
 
 val tvar_a_str = "'a"
-val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_z = ((tvar_a_str, 0), @{sort type})
 val tvar_a = TVar tvar_a_z
 val tvar_a_name = tvar_name tvar_a_z
 val itself_name = `make_fixed_type_const @{type_name itself}
@@ -2404,7 +2404,7 @@
 
 fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
     let
-      val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
+      val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, @{sort type}))
     in
       if forall (type_generalization thy T o result_type_of_decl) decls' then [decl]
       else decls
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -94,7 +94,7 @@
 
 fun make_tfree ctxt w =
   let val ww = "'" ^ w in
-    TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))
+    TFree (ww, the_default @{sort type} (Variable.def_sort ctxt (ww, ~1)))
   end
 
 exception ATP_CLASS of string list
@@ -126,7 +126,7 @@
              Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
              forces us to use a type parameter in all cases. *)
           Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
-            (if null clss then HOLogic.typeS else map class_of_atp_class clss))))
+            (if null clss then @{sort type} else map class_of_atp_class clss))))
   end
 
 fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
@@ -175,7 +175,7 @@
   else
     (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
 
-fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
+fun slack_fastype_of t = fastype_of t handle TERM _ => Type_Infer.anyT @{sort type}
 
 (* Cope with "tt(X) = X" atoms, where "X" is existentially quantified. *)
 fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
@@ -184,8 +184,8 @@
 val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
 val vampire_skolem_prefix = "sK"
 
-(* First-order translation. No types are known for variables. "HOLogic.typeT" should allow them to
-   be inferred. *)
+(* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}"
+   should allow them to be inferred. *)
 fun term_of_atp ctxt textual sym_tab =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -206,7 +206,7 @@
             if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then
               @{const True}
             else
-              list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
+              list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
           end
         else
           (case unprefix_and_unascii const_prefix s of
@@ -248,7 +248,8 @@
                        NONE)
                     |> (fn SOME T => T
                          | NONE =>
-                           map slack_fastype_of term_ts ---> the_default HOLogic.typeT opt_T)
+                           map slack_fastype_of term_ts --->
+                            the_default (Type_Infer.anyT @{sort type}) opt_T)
                   val t =
                     if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
                     else Const (unproxify_const s', T)
@@ -274,7 +275,7 @@
                   SOME T => map slack_fastype_of term_ts ---> T
                 | NONE =>
                   map slack_fastype_of ts --->
-                  (case tys of [ty] => typ_of_atp_type ctxt ty | _ => HOLogic.typeT))
+                  (case tys of [ty] => typ_of_atp_type ctxt ty | _ => Type_Infer.anyT @{sort type}))
               val t =
                 (case unprefix_and_unascii fixed_var_prefix s of
                   SOME s => Free (s, T)
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -138,15 +138,15 @@
                    forall inner from inners. idead = dead  *)
 
     val (oDs, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate odead HOLogic.typeS) lthy);
+      (Variable.invent_types (replicate odead @{sort type}) lthy);
     val (Dss, lthy2) = apfst (map (map TFree))
-      (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1);
+      (fold_map Variable.invent_types (map (fn n => replicate n @{sort type}) ideads) lthy1);
     val (Ass, lthy3) = apfst (replicate ilive o map TFree)
-      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
+      (Variable.invent_types (replicate ilive @{sort type}) lthy2);
     val As = if ilive > 0 then hd Ass else [];
     val Ass_repl = replicate olive As;
     val (Bs, names_lthy) = apfst (map TFree)
-      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
+      (Variable.invent_types (replicate ilive @{sort type}) lthy3);
     val Bss_repl = replicate olive Bs;
 
     val ((((fs', Qs'), Asets), xs), _) = names_lthy
@@ -363,11 +363,11 @@
     (* TODO: check 0 < n <= live *)
 
     val (Ds, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+      (Variable.invent_types (replicate dead @{sort type}) lthy);
     val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
-      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+      (Variable.invent_types (replicate live @{sort type}) lthy1);
     val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
-      (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
+      (Variable.invent_types (replicate (live - n) @{sort type}) lthy2);
 
     val ((Asets, lives), _(*names_lthy*)) = lthy
       |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
@@ -462,11 +462,11 @@
     (* TODO: check 0 < n *)
 
     val (Ds, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+      (Variable.invent_types (replicate dead @{sort type}) lthy);
     val ((newAs, As), lthy2) = apfst (chop n o map TFree)
-      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
+      (Variable.invent_types (replicate (n + live) @{sort type}) lthy1);
     val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
-      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
+      (Variable.invent_types (replicate (n + live) @{sort type}) lthy2);
 
     val (Asets, _(*names_lthy*)) = lthy
       |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
@@ -553,11 +553,11 @@
     fun unpermute xs = permute_like_unique (op =) dest src xs;
 
     val (Ds, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+      (Variable.invent_types (replicate dead @{sort type}) lthy);
     val (As, lthy2) = apfst (map TFree)
-      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+      (Variable.invent_types (replicate live @{sort type}) lthy1);
     val (Bs, _(*lthy3*)) = apfst (map TFree)
-      (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
+      (Variable.invent_types (replicate live @{sort type}) lthy2);
 
     val (Asets, _(*names_lthy*)) = lthy
       |> mk_Frees "A" (map HOLogic.mk_setT (permute As));
@@ -757,9 +757,9 @@
     val nwits = nwits_of_bnf bnf;
 
     val (As, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
+      (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy));
     val (Bs, _) = apfst (map TFree)
-      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+      (Variable.invent_types (replicate live @{sort type}) lthy1);
 
     val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
       |> mk_Frees' "f" (map2 (curry op -->) As Bs)
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -901,7 +901,7 @@
       end;
 
     val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs;
-    val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
+    val unsorted_Ass0 = map (map (resort_tfree @{sort type})) Ass0;
     val unsorted_As = Library.foldr1 (merge_type_args fp) unsorted_Ass0;
     val num_As = length unsorted_As;
 
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -963,7 +963,7 @@
     val (bs, mxs) = map_split (apfst fst) fixes;
     val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
 
-    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of
+    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of
         [] => ()
       | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
 
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -447,7 +447,7 @@
       | is_only_old_datatype _ = false;
 
     val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else ();
-    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ res_Ts) of
+    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ res_Ts) of
         [] => ()
       | (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", []));
 
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -148,7 +148,7 @@
 
 val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
 
-fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
+fun mk_TFrees n = mk_TFrees' (replicate n @{sort type});
 
 fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
 fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
@@ -169,7 +169,7 @@
 
 fun variant_tfrees ss =
   apfst (map TFree) o
-    variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
+    variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type});
 
 (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
 fun typ_subst_nonatomic [] = I
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -373,7 +373,7 @@
 
         fun mk_thm i =
           let
-            val Ts = map (TFree o rpair HOLogic.typeS) (Name.variant_list used (replicate i "'t"));
+            val Ts = map (TFree o rpair @{sort type}) (Name.variant_list used (replicate i "'t"));
             val f = Free ("f", Ts ---> U);
           in
             Goal.prove_sorry_global thy [] []
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -182,7 +182,7 @@
     val rec_result_Ts =
       map TFree
         (Name.variant_list used (replicate (length descr') "'t") ~~
-          replicate (length descr') HOLogic.typeS);
+          replicate (length descr') @{sort type});
 
     val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
@@ -251,7 +251,7 @@
     val recTs = Datatype_Aux.get_rec_types descr';
     val used = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
-    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
+    val T' = TFree (singleton (Name.variant_list used) "'t", @{sort type});
 
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
@@ -296,7 +296,7 @@
     val recTs = Datatype_Aux.get_rec_types descr';
     val used' = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
-    val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
+    val T' = TFree (singleton (Name.variant_list used') "'t", @{sort type});
     val P = Free ("P", T' --> HOLogic.boolT);
 
     fun make_split (((_, (_, _, constrs)), T), comb_t) =
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -36,7 +36,7 @@
       else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
 
     val rec_result_Ts = map (fn ((i, _), P) =>
-        if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
+        if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
       (descr ~~ pnames);
 
     fun make_pred i T U r x =
@@ -163,8 +163,8 @@
   let
     val ctxt = Proof_Context.init_global thy;
     val cert = cterm_of thy;
-    val rT = TFree ("'P", HOLogic.typeS);
-    val rT' = TVar (("'P", 0), HOLogic.typeS);
+    val rT = TFree ("'P", @{sort type});
+    val rT' = TVar (("'P", 0), @{sort type});
 
     fun make_casedist_prem T (cname, cargs) =
       let
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -278,7 +278,7 @@
     val recTs = Datatype_Aux.get_rec_types descr';
     val used = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
-    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
+    val T' = TFree (singleton (Name.variant_list used) "'t", @{sort type});
 
     fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' dt) ---> T';
 
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -73,7 +73,7 @@
         val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
       in
         HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
-          Const ("HOL.undefined", rT))
+          Const (@{const_name undefined}, rT))
         |> HOLogic.mk_Trueprop
         |> fold_rev Logic.all qs
       end
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -156,7 +156,7 @@
   end
 
 val add_function =
-  gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+  gen_add_function false Specification.check_spec (Type_Infer.anyT @{sort type})
 fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec "_::type" a b c d
 
 fun gen_function do_print prep default_constraint fixspec eqns config lthy =
@@ -170,7 +170,7 @@
   end
 
 val function =
-  gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+  gen_function false Specification.check_spec (Type_Infer.anyT @{sort type})
 fun function_cmd a b c int = gen_function int Specification.read_spec "_::type" a b c
 
 fun prepare_termination_proof prep_term raw_term_opt lthy =
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -347,7 +347,7 @@
         plural " " "s " not_defined ^ commas_quote not_defined)
 
     fun check_sorts ((fname, fT), _) =
-      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS)
+      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort type})
       orelse error (cat_lines
       ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
        Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -1053,7 +1053,7 @@
                     (Object_Logic.atomize_term thy prop)
         val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
                    |> map_types (map_type_tfree
-                                     (fn (s, []) => TFree (s, HOLogic.typeS)
+                                     (fn (s, []) => TFree (s, @{sort type})
                                        | x => TFree x))
         val _ =
           if debug then
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -920,7 +920,7 @@
     val Type ("fun", [T, T']) = fastype_of comb;
     val (Const (case_name, _), fs) = strip_comb comb
     val used = Term.add_tfree_names comb []
-    val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
+    val U = TFree (singleton (Name.variant_list used) "'t", @{sort type})
     val x = Free ("x", T)
     val f = Free ("f", T' --> U)
     fun apply_f f' =
@@ -947,8 +947,8 @@
     val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
     val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
     val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
-    val T' = TFree (tname', HOLogic.typeS)
-    val U = TFree (uname, HOLogic.typeS)
+    val T' = TFree (tname', @{sort type})
+    val U = TFree (uname, @{sort type})
     val y = Free (yname, U)
     val f' = absdummy (U --> T') (Bound 0 $ y)
     val th' = Thm.certify_instantiate
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -577,7 +577,7 @@
 val pat_var_prefix = "_"
 
 (* try "Long_Name.base_name" for shorter names *)
-fun massage_long_name s = if s = hd HOLogic.typeS then "T" else s
+fun massage_long_name s = if s = @{class type} then "T" else s
 
 val crude_str_of_sort =
   space_implode ":" o map massage_long_name o subtract (op =) @{sort type}
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/TFL/usyntax.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -104,7 +104,7 @@
  *
  *---------------------------------------------------------------------------*)
 val mk_prim_vartype = TVar;
-fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS);
+fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type});
 
 (* But internally, it's useful *)
 fun dest_vtype (TVar x) = x
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -131,7 +131,7 @@
         fun proc_single prop =
             let
                 val frees = Misc_Legacy.term_frees prop
-                val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
+                val _ = forall (fn v => Sign.of_sort thy (type_of v,@{sort type})) frees
                   orelse error "Specificaton: Only free variables of sort 'type' allowed"
                 val prop_closed = close_form prop
             in
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/hologic.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -6,8 +6,6 @@
 
 signature HOLOGIC =
 sig
-  val typeS: sort
-  val typeT: typ
   val id_const: typ -> term
   val mk_comp: term * term -> term
   val boolN: string
@@ -141,12 +139,6 @@
 structure HOLogic: HOLOGIC =
 struct
 
-(* HOL syntax *)
-
-val typeS: sort = ["HOL.type"];
-val typeT = Type_Infer.anyT typeS;
-
-
 (* functions *)
 
 fun id_const T = Const ("Fun.id", T --> T);
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -53,8 +53,8 @@
       | _ => vs)) (Term.add_vars prop []) [];
 
 val attach_typeS = map_types (map_atyps
-  (fn TFree (s, []) => TFree (s, HOLogic.typeS)
-    | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
+  (fn TFree (s, []) => TFree (s, @{sort type})
+    | TVar (ixn, []) => TVar (ixn, @{sort type})
     | T => T));
 
 fun dt_of_intrs thy vs nparms intrs =
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -1819,7 +1819,7 @@
     val all_vars = parent_vars @ vars;
     val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
 
-    val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
+    val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", @{sort type});
     val moreT = TFree zeta;
     val more = Free (moreN, moreT);
     val full_moreN = full (Binding.name moreN);
diff -r 83b3c110f22d -r a2dd9200854d src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/transfer.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -467,7 +467,7 @@
       | go _ ctxt = dummy ctxt
   in
     go t ctxt |> fst |> Syntax.check_term ctxt |>
-      map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS)))
+      map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
   end
 
 (** Monotonicity analysis **)
@@ -544,7 +544,7 @@
     val relT = @{typ "bool => bool => bool"}
     val idx = Thm.maxidx_of thm + 1
     val thy = Proof_Context.theory_of ctxt
-    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
+    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
     fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
   in
     thm
@@ -569,7 +569,7 @@
     val relT = @{typ "bool => bool => bool"}
     val idx = Thm.maxidx_of thm + 1
     val thy = Proof_Context.theory_of ctxt
-    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
+    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
     fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
   in
     thm