more antiquotations;
authorwenzelm
Sat Mar 22 18:19:57 2014 +0100 (2014-03-22)
changeset 56254a2dd9200854d
parent 56253 83b3c110f22d
child 56255 968667bbb8d2
more antiquotations;
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/record.ML
src/HOL/Tools/transfer.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -434,7 +434,7 @@
     1.4  fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
     1.5  
     1.6  val tvar_a_str = "'a"
     1.7 -val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
     1.8 +val tvar_a_z = ((tvar_a_str, 0), @{sort type})
     1.9  val tvar_a = TVar tvar_a_z
    1.10  val tvar_a_name = tvar_name tvar_a_z
    1.11  val itself_name = `make_fixed_type_const @{type_name itself}
    1.12 @@ -2404,7 +2404,7 @@
    1.13  
    1.14  fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
    1.15      let
    1.16 -      val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
    1.17 +      val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, @{sort type}))
    1.18      in
    1.19        if forall (type_generalization thy T o result_type_of_decl) decls' then [decl]
    1.20        else decls
     2.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Mar 22 18:16:54 2014 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Mar 22 18:19:57 2014 +0100
     2.3 @@ -94,7 +94,7 @@
     2.4  
     2.5  fun make_tfree ctxt w =
     2.6    let val ww = "'" ^ w in
     2.7 -    TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))
     2.8 +    TFree (ww, the_default @{sort type} (Variable.def_sort ctxt (ww, ~1)))
     2.9    end
    2.10  
    2.11  exception ATP_CLASS of string list
    2.12 @@ -126,7 +126,7 @@
    2.13               Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
    2.14               forces us to use a type parameter in all cases. *)
    2.15            Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
    2.16 -            (if null clss then HOLogic.typeS else map class_of_atp_class clss))))
    2.17 +            (if null clss then @{sort type} else map class_of_atp_class clss))))
    2.18    end
    2.19  
    2.20  fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
    2.21 @@ -175,7 +175,7 @@
    2.22    else
    2.23      (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
    2.24  
    2.25 -fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
    2.26 +fun slack_fastype_of t = fastype_of t handle TERM _ => Type_Infer.anyT @{sort type}
    2.27  
    2.28  (* Cope with "tt(X) = X" atoms, where "X" is existentially quantified. *)
    2.29  fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
    2.30 @@ -184,8 +184,8 @@
    2.31  val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
    2.32  val vampire_skolem_prefix = "sK"
    2.33  
    2.34 -(* First-order translation. No types are known for variables. "HOLogic.typeT" should allow them to
    2.35 -   be inferred. *)
    2.36 +(* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}"
    2.37 +   should allow them to be inferred. *)
    2.38  fun term_of_atp ctxt textual sym_tab =
    2.39    let
    2.40      val thy = Proof_Context.theory_of ctxt
    2.41 @@ -206,7 +206,7 @@
    2.42              if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then
    2.43                @{const True}
    2.44              else
    2.45 -              list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
    2.46 +              list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
    2.47            end
    2.48          else
    2.49            (case unprefix_and_unascii const_prefix s of
    2.50 @@ -248,7 +248,8 @@
    2.51                         NONE)
    2.52                      |> (fn SOME T => T
    2.53                           | NONE =>
    2.54 -                           map slack_fastype_of term_ts ---> the_default HOLogic.typeT opt_T)
    2.55 +                           map slack_fastype_of term_ts --->
    2.56 +                            the_default (Type_Infer.anyT @{sort type}) opt_T)
    2.57                    val t =
    2.58                      if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
    2.59                      else Const (unproxify_const s', T)
    2.60 @@ -274,7 +275,7 @@
    2.61                    SOME T => map slack_fastype_of term_ts ---> T
    2.62                  | NONE =>
    2.63                    map slack_fastype_of ts --->
    2.64 -                  (case tys of [ty] => typ_of_atp_type ctxt ty | _ => HOLogic.typeT))
    2.65 +                  (case tys of [ty] => typ_of_atp_type ctxt ty | _ => Type_Infer.anyT @{sort type}))
    2.66                val t =
    2.67                  (case unprefix_and_unascii fixed_var_prefix s of
    2.68                    SOME s => Free (s, T)
     3.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Sat Mar 22 18:16:54 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sat Mar 22 18:19:57 2014 +0100
     3.3 @@ -138,15 +138,15 @@
     3.4                     forall inner from inners. idead = dead  *)
     3.5  
     3.6      val (oDs, lthy1) = apfst (map TFree)
     3.7 -      (Variable.invent_types (replicate odead HOLogic.typeS) lthy);
     3.8 +      (Variable.invent_types (replicate odead @{sort type}) lthy);
     3.9      val (Dss, lthy2) = apfst (map (map TFree))
    3.10 -      (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1);
    3.11 +      (fold_map Variable.invent_types (map (fn n => replicate n @{sort type}) ideads) lthy1);
    3.12      val (Ass, lthy3) = apfst (replicate ilive o map TFree)
    3.13 -      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
    3.14 +      (Variable.invent_types (replicate ilive @{sort type}) lthy2);
    3.15      val As = if ilive > 0 then hd Ass else [];
    3.16      val Ass_repl = replicate olive As;
    3.17      val (Bs, names_lthy) = apfst (map TFree)
    3.18 -      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
    3.19 +      (Variable.invent_types (replicate ilive @{sort type}) lthy3);
    3.20      val Bss_repl = replicate olive Bs;
    3.21  
    3.22      val ((((fs', Qs'), Asets), xs), _) = names_lthy
    3.23 @@ -363,11 +363,11 @@
    3.24      (* TODO: check 0 < n <= live *)
    3.25  
    3.26      val (Ds, lthy1) = apfst (map TFree)
    3.27 -      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
    3.28 +      (Variable.invent_types (replicate dead @{sort type}) lthy);
    3.29      val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
    3.30 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
    3.31 +      (Variable.invent_types (replicate live @{sort type}) lthy1);
    3.32      val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
    3.33 -      (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
    3.34 +      (Variable.invent_types (replicate (live - n) @{sort type}) lthy2);
    3.35  
    3.36      val ((Asets, lives), _(*names_lthy*)) = lthy
    3.37        |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
    3.38 @@ -462,11 +462,11 @@
    3.39      (* TODO: check 0 < n *)
    3.40  
    3.41      val (Ds, lthy1) = apfst (map TFree)
    3.42 -      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
    3.43 +      (Variable.invent_types (replicate dead @{sort type}) lthy);
    3.44      val ((newAs, As), lthy2) = apfst (chop n o map TFree)
    3.45 -      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
    3.46 +      (Variable.invent_types (replicate (n + live) @{sort type}) lthy1);
    3.47      val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
    3.48 -      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
    3.49 +      (Variable.invent_types (replicate (n + live) @{sort type}) lthy2);
    3.50  
    3.51      val (Asets, _(*names_lthy*)) = lthy
    3.52        |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
    3.53 @@ -553,11 +553,11 @@
    3.54      fun unpermute xs = permute_like_unique (op =) dest src xs;
    3.55  
    3.56      val (Ds, lthy1) = apfst (map TFree)
    3.57 -      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
    3.58 +      (Variable.invent_types (replicate dead @{sort type}) lthy);
    3.59      val (As, lthy2) = apfst (map TFree)
    3.60 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
    3.61 +      (Variable.invent_types (replicate live @{sort type}) lthy1);
    3.62      val (Bs, _(*lthy3*)) = apfst (map TFree)
    3.63 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
    3.64 +      (Variable.invent_types (replicate live @{sort type}) lthy2);
    3.65  
    3.66      val (Asets, _(*names_lthy*)) = lthy
    3.67        |> mk_Frees "A" (map HOLogic.mk_setT (permute As));
    3.68 @@ -757,9 +757,9 @@
    3.69      val nwits = nwits_of_bnf bnf;
    3.70  
    3.71      val (As, lthy1) = apfst (map TFree)
    3.72 -      (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
    3.73 +      (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy));
    3.74      val (Bs, _) = apfst (map TFree)
    3.75 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
    3.76 +      (Variable.invent_types (replicate live @{sort type}) lthy1);
    3.77  
    3.78      val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
    3.79        |> mk_Frees' "f" (map2 (curry op -->) As Bs)
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sat Mar 22 18:16:54 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sat Mar 22 18:19:57 2014 +0100
     4.3 @@ -901,7 +901,7 @@
     4.4        end;
     4.5  
     4.6      val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs;
     4.7 -    val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
     4.8 +    val unsorted_Ass0 = map (map (resort_tfree @{sort type})) Ass0;
     4.9      val unsorted_As = Library.foldr1 (merge_type_args fp) unsorted_Ass0;
    4.10      val num_As = length unsorted_As;
    4.11  
     5.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Mar 22 18:16:54 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Mar 22 18:19:57 2014 +0100
     5.3 @@ -963,7 +963,7 @@
     5.4      val (bs, mxs) = map_split (apfst fst) fixes;
     5.5      val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
     5.6  
     5.7 -    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of
     5.8 +    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of
     5.9          [] => ()
    5.10        | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
    5.11  
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Mar 22 18:16:54 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Mar 22 18:19:57 2014 +0100
     6.3 @@ -447,7 +447,7 @@
     6.4        | is_only_old_datatype _ = false;
     6.5  
     6.6      val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else ();
     6.7 -    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ res_Ts) of
     6.8 +    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ res_Ts) of
     6.9          [] => ()
    6.10        | (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", []));
    6.11  
     7.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sat Mar 22 18:16:54 2014 +0100
     7.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sat Mar 22 18:19:57 2014 +0100
     7.3 @@ -148,7 +148,7 @@
     7.4  
     7.5  val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
     7.6  
     7.7 -fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
     7.8 +fun mk_TFrees n = mk_TFrees' (replicate n @{sort type});
     7.9  
    7.10  fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
    7.11  fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
    7.12 @@ -169,7 +169,7 @@
    7.13  
    7.14  fun variant_tfrees ss =
    7.15    apfst (map TFree) o
    7.16 -    variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
    7.17 +    variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type});
    7.18  
    7.19  (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
    7.20  fun typ_subst_nonatomic [] = I
     8.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 22 18:16:54 2014 +0100
     8.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 22 18:19:57 2014 +0100
     8.3 @@ -373,7 +373,7 @@
     8.4  
     8.5          fun mk_thm i =
     8.6            let
     8.7 -            val Ts = map (TFree o rpair HOLogic.typeS) (Name.variant_list used (replicate i "'t"));
     8.8 +            val Ts = map (TFree o rpair @{sort type}) (Name.variant_list used (replicate i "'t"));
     8.9              val f = Free ("f", Ts ---> U);
    8.10            in
    8.11              Goal.prove_sorry_global thy [] []
     9.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Mar 22 18:16:54 2014 +0100
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Mar 22 18:19:57 2014 +0100
     9.3 @@ -182,7 +182,7 @@
     9.4      val rec_result_Ts =
     9.5        map TFree
     9.6          (Name.variant_list used (replicate (length descr') "'t") ~~
     9.7 -          replicate (length descr') HOLogic.typeS);
     9.8 +          replicate (length descr') @{sort type});
     9.9  
    9.10      val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
    9.11        map (fn (_, cargs) =>
    9.12 @@ -251,7 +251,7 @@
    9.13      val recTs = Datatype_Aux.get_rec_types descr';
    9.14      val used = fold Term.add_tfree_namesT recTs [];
    9.15      val newTs = take (length (hd descr)) recTs;
    9.16 -    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
    9.17 +    val T' = TFree (singleton (Name.variant_list used) "'t", @{sort type});
    9.18  
    9.19      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
    9.20        map (fn (_, cargs) =>
    9.21 @@ -296,7 +296,7 @@
    9.22      val recTs = Datatype_Aux.get_rec_types descr';
    9.23      val used' = fold Term.add_tfree_namesT recTs [];
    9.24      val newTs = take (length (hd descr)) recTs;
    9.25 -    val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
    9.26 +    val T' = TFree (singleton (Name.variant_list used') "'t", @{sort type});
    9.27      val P = Free ("P", T' --> HOLogic.boolT);
    9.28  
    9.29      fun make_split (((_, (_, _, constrs)), T), comb_t) =
    10.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Mar 22 18:16:54 2014 +0100
    10.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Mar 22 18:19:57 2014 +0100
    10.3 @@ -36,7 +36,7 @@
    10.4        else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
    10.5  
    10.6      val rec_result_Ts = map (fn ((i, _), P) =>
    10.7 -        if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
    10.8 +        if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
    10.9        (descr ~~ pnames);
   10.10  
   10.11      fun make_pred i T U r x =
   10.12 @@ -163,8 +163,8 @@
   10.13    let
   10.14      val ctxt = Proof_Context.init_global thy;
   10.15      val cert = cterm_of thy;
   10.16 -    val rT = TFree ("'P", HOLogic.typeS);
   10.17 -    val rT' = TVar (("'P", 0), HOLogic.typeS);
   10.18 +    val rT = TFree ("'P", @{sort type});
   10.19 +    val rT' = TVar (("'P", 0), @{sort type});
   10.20  
   10.21      fun make_casedist_prem T (cname, cargs) =
   10.22        let
    11.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Mar 22 18:16:54 2014 +0100
    11.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Mar 22 18:19:57 2014 +0100
    11.3 @@ -278,7 +278,7 @@
    11.4      val recTs = Datatype_Aux.get_rec_types descr';
    11.5      val used = fold Term.add_tfree_namesT recTs [];
    11.6      val newTs = take (length (hd descr)) recTs;
    11.7 -    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
    11.8 +    val T' = TFree (singleton (Name.variant_list used) "'t", @{sort type});
    11.9  
   11.10      fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' dt) ---> T';
   11.11  
    12.1 --- a/src/HOL/Tools/Function/fun.ML	Sat Mar 22 18:16:54 2014 +0100
    12.2 +++ b/src/HOL/Tools/Function/fun.ML	Sat Mar 22 18:19:57 2014 +0100
    12.3 @@ -73,7 +73,7 @@
    12.4          val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
    12.5        in
    12.6          HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
    12.7 -          Const ("HOL.undefined", rT))
    12.8 +          Const (@{const_name undefined}, rT))
    12.9          |> HOLogic.mk_Trueprop
   12.10          |> fold_rev Logic.all qs
   12.11        end
    13.1 --- a/src/HOL/Tools/Function/function.ML	Sat Mar 22 18:16:54 2014 +0100
    13.2 +++ b/src/HOL/Tools/Function/function.ML	Sat Mar 22 18:19:57 2014 +0100
    13.3 @@ -156,7 +156,7 @@
    13.4    end
    13.5  
    13.6  val add_function =
    13.7 -  gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
    13.8 +  gen_add_function false Specification.check_spec (Type_Infer.anyT @{sort type})
    13.9  fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec "_::type" a b c d
   13.10  
   13.11  fun gen_function do_print prep default_constraint fixspec eqns config lthy =
   13.12 @@ -170,7 +170,7 @@
   13.13    end
   13.14  
   13.15  val function =
   13.16 -  gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
   13.17 +  gen_function false Specification.check_spec (Type_Infer.anyT @{sort type})
   13.18  fun function_cmd a b c int = gen_function int Specification.read_spec "_::type" a b c
   13.19  
   13.20  fun prepare_termination_proof prep_term raw_term_opt lthy =
    14.1 --- a/src/HOL/Tools/Function/function_common.ML	Sat Mar 22 18:16:54 2014 +0100
    14.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sat Mar 22 18:19:57 2014 +0100
    14.3 @@ -347,7 +347,7 @@
    14.4          plural " " "s " not_defined ^ commas_quote not_defined)
    14.5  
    14.6      fun check_sorts ((fname, fT), _) =
    14.7 -      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS)
    14.8 +      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort type})
    14.9        orelse error (cat_lines
   14.10        ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
   14.11         Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
    15.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Mar 22 18:16:54 2014 +0100
    15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Mar 22 18:19:57 2014 +0100
    15.3 @@ -1053,7 +1053,7 @@
    15.4                      (Object_Logic.atomize_term thy prop)
    15.5          val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
    15.6                     |> map_types (map_type_tfree
    15.7 -                                     (fn (s, []) => TFree (s, HOLogic.typeS)
    15.8 +                                     (fn (s, []) => TFree (s, @{sort type})
    15.9                                         | x => TFree x))
   15.10          val _ =
   15.11            if debug then
    16.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Mar 22 18:16:54 2014 +0100
    16.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Mar 22 18:19:57 2014 +0100
    16.3 @@ -920,7 +920,7 @@
    16.4      val Type ("fun", [T, T']) = fastype_of comb;
    16.5      val (Const (case_name, _), fs) = strip_comb comb
    16.6      val used = Term.add_tfree_names comb []
    16.7 -    val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
    16.8 +    val U = TFree (singleton (Name.variant_list used) "'t", @{sort type})
    16.9      val x = Free ("x", T)
   16.10      val f = Free ("f", T' --> U)
   16.11      fun apply_f f' =
   16.12 @@ -947,8 +947,8 @@
   16.13      val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
   16.14      val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
   16.15      val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
   16.16 -    val T' = TFree (tname', HOLogic.typeS)
   16.17 -    val U = TFree (uname, HOLogic.typeS)
   16.18 +    val T' = TFree (tname', @{sort type})
   16.19 +    val U = TFree (uname, @{sort type})
   16.20      val y = Free (yname, U)
   16.21      val f' = absdummy (U --> T') (Bound 0 $ y)
   16.22      val th' = Thm.certify_instantiate
    17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Mar 22 18:16:54 2014 +0100
    17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Mar 22 18:19:57 2014 +0100
    17.3 @@ -577,7 +577,7 @@
    17.4  val pat_var_prefix = "_"
    17.5  
    17.6  (* try "Long_Name.base_name" for shorter names *)
    17.7 -fun massage_long_name s = if s = hd HOLogic.typeS then "T" else s
    17.8 +fun massage_long_name s = if s = @{class type} then "T" else s
    17.9  
   17.10  val crude_str_of_sort =
   17.11    space_implode ":" o map massage_long_name o subtract (op =) @{sort type}
    18.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Sat Mar 22 18:16:54 2014 +0100
    18.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Sat Mar 22 18:19:57 2014 +0100
    18.3 @@ -104,7 +104,7 @@
    18.4   *
    18.5   *---------------------------------------------------------------------------*)
    18.6  val mk_prim_vartype = TVar;
    18.7 -fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS);
    18.8 +fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type});
    18.9  
   18.10  (* But internally, it's useful *)
   18.11  fun dest_vtype (TVar x) = x
    19.1 --- a/src/HOL/Tools/choice_specification.ML	Sat Mar 22 18:16:54 2014 +0100
    19.2 +++ b/src/HOL/Tools/choice_specification.ML	Sat Mar 22 18:19:57 2014 +0100
    19.3 @@ -131,7 +131,7 @@
    19.4          fun proc_single prop =
    19.5              let
    19.6                  val frees = Misc_Legacy.term_frees prop
    19.7 -                val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
    19.8 +                val _ = forall (fn v => Sign.of_sort thy (type_of v,@{sort type})) frees
    19.9                    orelse error "Specificaton: Only free variables of sort 'type' allowed"
   19.10                  val prop_closed = close_form prop
   19.11              in
    20.1 --- a/src/HOL/Tools/hologic.ML	Sat Mar 22 18:16:54 2014 +0100
    20.2 +++ b/src/HOL/Tools/hologic.ML	Sat Mar 22 18:19:57 2014 +0100
    20.3 @@ -6,8 +6,6 @@
    20.4  
    20.5  signature HOLOGIC =
    20.6  sig
    20.7 -  val typeS: sort
    20.8 -  val typeT: typ
    20.9    val id_const: typ -> term
   20.10    val mk_comp: term * term -> term
   20.11    val boolN: string
   20.12 @@ -141,12 +139,6 @@
   20.13  structure HOLogic: HOLOGIC =
   20.14  struct
   20.15  
   20.16 -(* HOL syntax *)
   20.17 -
   20.18 -val typeS: sort = ["HOL.type"];
   20.19 -val typeT = Type_Infer.anyT typeS;
   20.20 -
   20.21 -
   20.22  (* functions *)
   20.23  
   20.24  fun id_const T = Const ("Fun.id", T --> T);
    21.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 22 18:16:54 2014 +0100
    21.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 22 18:19:57 2014 +0100
    21.3 @@ -53,8 +53,8 @@
    21.4        | _ => vs)) (Term.add_vars prop []) [];
    21.5  
    21.6  val attach_typeS = map_types (map_atyps
    21.7 -  (fn TFree (s, []) => TFree (s, HOLogic.typeS)
    21.8 -    | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
    21.9 +  (fn TFree (s, []) => TFree (s, @{sort type})
   21.10 +    | TVar (ixn, []) => TVar (ixn, @{sort type})
   21.11      | T => T));
   21.12  
   21.13  fun dt_of_intrs thy vs nparms intrs =
    22.1 --- a/src/HOL/Tools/record.ML	Sat Mar 22 18:16:54 2014 +0100
    22.2 +++ b/src/HOL/Tools/record.ML	Sat Mar 22 18:19:57 2014 +0100
    22.3 @@ -1819,7 +1819,7 @@
    22.4      val all_vars = parent_vars @ vars;
    22.5      val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
    22.6  
    22.7 -    val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
    22.8 +    val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", @{sort type});
    22.9      val moreT = TFree zeta;
   22.10      val more = Free (moreN, moreT);
   22.11      val full_moreN = full (Binding.name moreN);
    23.1 --- a/src/HOL/Tools/transfer.ML	Sat Mar 22 18:16:54 2014 +0100
    23.2 +++ b/src/HOL/Tools/transfer.ML	Sat Mar 22 18:19:57 2014 +0100
    23.3 @@ -467,7 +467,7 @@
    23.4        | go _ ctxt = dummy ctxt
    23.5    in
    23.6      go t ctxt |> fst |> Syntax.check_term ctxt |>
    23.7 -      map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS)))
    23.8 +      map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
    23.9    end
   23.10  
   23.11  (** Monotonicity analysis **)
   23.12 @@ -544,7 +544,7 @@
   23.13      val relT = @{typ "bool => bool => bool"}
   23.14      val idx = Thm.maxidx_of thm + 1
   23.15      val thy = Proof_Context.theory_of ctxt
   23.16 -    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
   23.17 +    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
   23.18      fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
   23.19    in
   23.20      thm
   23.21 @@ -569,7 +569,7 @@
   23.22      val relT = @{typ "bool => bool => bool"}
   23.23      val idx = Thm.maxidx_of thm + 1
   23.24      val thy = Proof_Context.theory_of ctxt
   23.25 -    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
   23.26 +    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
   23.27      fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
   23.28    in
   23.29      thm