# HG changeset patch
# User wenzelm
# Date 1395522026 -3600
# Node ID fec233e7f67d9aec1145c2976fcb90745db7ab72
# Parent  67dc9549fa157355cd5a7a43d0e2cbff4d899b73# Parent  589fafcc7cb63399d81c13036e6068f502d38f64
merged

diff -r 67dc9549fa15 -r fec233e7f67d src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/CTT/CTT.thy	Sat Mar 22 22:00:26 2014 +0100
@@ -328,9 +328,9 @@
 
 local
 
-fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
-  | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
-  | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
+fun is_rigid_elem (Const(@{const_name Elem},_) $ a $ _) = not(is_Var (head_of a))
+  | is_rigid_elem (Const(@{const_name Eqelem},_) $ a $ _ $ _) = not(is_Var (head_of a))
+  | is_rigid_elem (Const(@{const_name Type},_) $ a) = not(is_Var (head_of a))
   | is_rigid_elem _ = false
 
 in
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -404,7 +404,7 @@
     : (Domain_Take_Proofs.iso_info list
        * Domain_Take_Proofs.take_induct_info) * theory =
   let
-    val _ = Theory.requires thy "Domain" "domain isomorphisms"
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "domain isomorphisms"
 
     (* this theory is used just for parsing *)
     val tmp_thy = thy |>
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -140,7 +140,7 @@
 
 fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy =
   let
-    val _ = Theory.requires thy "Cpodef" "cpodefs"
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "cpodefs"
 
     (*rhs*)
     val tmp_ctxt =
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -84,7 +84,7 @@
       (thy: theory)
     : (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory =
   let
-    val _ = Theory.requires thy "Domain" "domaindefs"
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "domaindefs"
 
     (*rhs*)
     val tmp_ctxt =
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Import/import_rule.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -409,7 +409,7 @@
           end
       | process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state)
       | process (thy, state) (#"t", [n]) =
-          setty (ctyp_of thy (TFree ("'" ^ (transl_qm n), ["HOL.type"]))) (thy, state)
+          setty (ctyp_of thy (TFree ("'" ^ (transl_qm n), @{sort type}))) (thy, state)
       | process (thy, state) (#"a", n :: l) =
           fold_map getty l (thy, state) |>>
             (fn tys => ctyp_of thy (Type (gettyname n thy, map typ_of tys))) |-> setty
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Library/bnf_decl.ML
--- a/src/HOL/Library/bnf_decl.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Library/bnf_decl.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -94,7 +94,7 @@
 
 val bnf_decl = prepare_decl (K I) (K I);
 
-fun read_constraint _ NONE = HOLogic.typeS
+fun read_constraint _ NONE = @{sort type}
   | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
 
 val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ;
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Library/refute.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -4,11 +4,6 @@
 Finite model generation for HOL formulas, using a SAT solver.
 *)
 
-(* ------------------------------------------------------------------------- *)
-(* Declares the 'REFUTE' signature as well as a structure 'Refute'.          *)
-(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'.  *)
-(* ------------------------------------------------------------------------- *)
-
 signature REFUTE =
 sig
 
@@ -579,7 +574,7 @@
           Type ("fun", [@{typ nat}, @{typ nat}])])) => t
       | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
           Type ("fun", [@{typ nat}, @{typ nat}])])) => t
-      | Const (@{const_name List.append}, _) => t
+      | Const (@{const_name append}, _) => t
 (* UNSOUND
       | Const (@{const_name lfp}, _) => t
       | Const (@{const_name gfp}, _) => t
@@ -638,6 +633,16 @@
 (* To avoid collecting the same axiom multiple times, we use an           *)
 (* accumulator 'axs' which contains all axioms collected so far.          *)
 
+local
+
+fun get_axiom thy xname =
+  Name_Space.check (Context.Theory thy) (Theory.axiom_table thy) (xname, Position.none);
+
+val the_eq_trivial = get_axiom @{theory HOL} "the_eq_trivial";
+val someI = get_axiom @{theory Hilbert_Choice} "someI";
+
+in
+
 fun collect_axioms ctxt t =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -684,11 +689,11 @@
     and collect_type_axioms T axs =
       case T of
       (* simple types *)
-        Type ("prop", []) => axs
-      | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
+        Type (@{type_name prop}, []) => axs
+      | Type (@{type_name fun}, [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
       | Type (@{type_name set}, [T1]) => collect_type_axioms T1 axs
       (* axiomatic type classes *)
-      | Type ("itself", [T1]) => collect_type_axioms T1 axs
+      | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
       | Type (s, Ts) =>
         (case Datatype.get_info thy s of
           SOME _ =>  (* inductive datatype *)
@@ -724,17 +729,15 @@
       | Const (@{const_name undefined}, T) => collect_type_axioms T axs
       | Const (@{const_name The}, T) =>
           let
-            val ax = specialize_type thy (@{const_name The}, T)
-              (the (AList.lookup (op =) axioms "HOL.the_eq_trivial"))
+            val ax = specialize_type thy (@{const_name The}, T) (#2 the_eq_trivial)
           in
-            collect_this_axiom ("HOL.the_eq_trivial", ax) axs
+            collect_this_axiom (#1 the_eq_trivial, ax) axs
           end
       | Const (@{const_name Hilbert_Choice.Eps}, T) =>
           let
-            val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T)
-              (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))
+            val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) (#2 someI)
           in
-            collect_this_axiom ("Hilbert_Choice.someI", ax) axs
+            collect_this_axiom (#1 someI, ax) axs
           end
       | Const (@{const_name All}, T) => collect_type_axioms T axs
       | Const (@{const_name Ex}, T) => collect_type_axioms T axs
@@ -761,7 +764,7 @@
       | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},
         Type ("fun", [@{typ nat}, @{typ nat}])])) =>
           collect_type_axioms T axs
-      | Const (@{const_name List.append}, T) => collect_type_axioms T axs
+      | Const (@{const_name append}, T) => collect_type_axioms T axs
 (* UNSOUND
       | Const (@{const_name lfp}, T) => collect_type_axioms T axs
       | Const (@{const_name gfp}, T) => collect_type_axioms T axs
@@ -806,6 +809,8 @@
     result
   end;
 
+end;
+
 (* ------------------------------------------------------------------------- *)
 (* ground_types: collects all ground types in a term (including argument     *)
 (*               types of other types), suppressing duplicates.  Does not    *)
@@ -819,8 +824,8 @@
     val thy = Proof_Context.theory_of ctxt
     fun collect_types T acc =
       (case T of
-        Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
-      | Type ("prop", []) => acc
+        Type (@{type_name fun}, [T1, T2]) => collect_types T1 (collect_types T2 acc)
+      | Type (@{type_name prop}, []) => acc
       | Type (@{type_name set}, [T1]) => collect_types T1 acc
       | Type (s, Ts) =>
           (case Datatype.get_info thy s of
@@ -2620,11 +2625,12 @@
 
 fun List_append_interpreter ctxt model args t =
   case t of
-    Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun",
-        [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
+    Const (@{const_name append},
+      Type (@{type_name fun}, [Type (@{type_name list}, [T]),
+        Type (@{type_name fun}, [Type (@{type_name list}, [_]), Type (@{type_name list}, [_])])])) =>
       let
         val size_elem = size_of_type ctxt model T
-        val size_list = size_of_type ctxt model (Type ("List.list", [T]))
+        val size_list = size_of_type ctxt model (Type (@{type_name list}, [T]))
         (* maximal length of lists; 0 if we only consider the empty list *)
         val list_length =
           let
@@ -2866,7 +2872,7 @@
         in
           SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set)
         end
-    | Type ("prop", []) =>
+    | Type (@{type_name prop}, []) =>
         (case index_from_interpretation intr of
           ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
         | 0  => SOME (HOLogic.mk_Trueprop @{term True})
@@ -3031,7 +3037,7 @@
 (*       applied before the 'stlc_interpreter' breaks the term apart into    *)
 (*       subterms that are then passed to other interpreters!                *)
 (* ------------------------------------------------------------------------- *)
-
+(* FIXME formal @{const_name} for some entries (!??) *)
 val setup =
    add_interpreter "stlc"    stlc_interpreter #>
    add_interpreter "Pure"    Pure_interpreter #>
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Library/simps_case_conv.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -152,13 +152,12 @@
 
 fun was_split t =
   let
-    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq
-              o fst o HOLogic.dest_imp
+    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp
     val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
-    fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t
+    fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t
       | dest_alls t = t
   in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
-        handle TERM _ => false
+  handle TERM _ => false
 
 fun apply_split ctxt split thm = Seq.of_list
   let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Sat Mar 22 22:00:26 2014 +0100
@@ -239,6 +239,6 @@
 lemmas arith = arith_simps rel_simps diff_nat_numeral nat_0
   nat_neg_numeral powerarith floatarith not_false_eq_true not_true_eq_false
 
-ML_file "~~/src/HOL/Tools/float_arith.ML"
+ML_file "float_arith.ML"
 
 end
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Matrix_LP/float_arith.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix_LP/float_arith.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -0,0 +1,221 @@
+(*  Title:      HOL/Matrix_LP/float_arith.ML
+    Author:     Steven Obua
+*)
+
+signature FLOAT_ARITH =
+sig
+  exception Destruct_floatstr of string
+  val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
+
+  exception Floating_point of string
+  val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float
+  val approx_decstr_by_bin: int -> string -> Float.float * Float.float
+
+  val mk_float: Float.float -> term
+  val dest_float: term -> Float.float
+
+  val approx_float: int -> (Float.float * Float.float -> Float.float * Float.float)
+    -> string -> term * term
+end;
+
+structure FloatArith : FLOAT_ARITH =
+struct
+
+exception Destruct_floatstr of string;
+
+fun destruct_floatstr isDigit isExp number =
+  let
+    val numlist = filter (not o Char.isSpace) (String.explode number)
+
+    fun countsigns ((#"+")::cs) = countsigns cs
+      | countsigns ((#"-")::cs) =
+      let
+        val (positive, rest) = countsigns cs
+      in
+        (not positive, rest)
+      end
+      | countsigns cs = (true, cs)
+
+    fun readdigits [] = ([], [])
+      | readdigits (q as c::cs) =
+      if (isDigit c) then
+        let
+          val (digits, rest) = readdigits cs
+        in
+          (c::digits, rest)
+        end
+      else
+        ([], q)
+
+    fun readfromexp_helper cs =
+      let
+        val (positive, rest) = countsigns cs
+        val (digits, rest') = readdigits rest
+      in
+        case rest' of
+          [] => (positive, digits)
+          | _ => raise (Destruct_floatstr number)
+      end
+
+    fun readfromexp [] = (true, [])
+      | readfromexp (c::cs) =
+      if isExp c then
+        readfromexp_helper cs
+      else
+        raise (Destruct_floatstr number)
+
+    fun readfromdot [] = ([], readfromexp [])
+      | readfromdot ((#".")::cs) =
+      let
+        val (digits, rest) = readdigits cs
+        val exp = readfromexp rest
+      in
+        (digits, exp)
+      end
+      | readfromdot cs = readfromdot ((#".")::cs)
+
+    val (positive, numlist) = countsigns numlist
+    val (digits1, numlist) = readdigits numlist
+     val (digits2, exp) = readfromdot numlist
+  in
+    (positive, String.implode digits1, String.implode digits2, fst exp, String.implode (snd exp))
+  end
+
+exception Floating_point of string;
+
+val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
+fun exp5 x = Integer.pow x 5;
+fun exp10 x = Integer.pow x 10;
+fun exp2 x = Integer.pow x 2;
+
+fun find_most_significant q r =
+  let
+    fun int2real i =
+      case (Real.fromString o string_of_int) i of
+        SOME r => r
+        | NONE => raise (Floating_point "int2real")
+    fun subtract (q, r) (q', r') =
+      if r <= r' then
+        (q - q' * exp10 (r' - r), r)
+      else
+        (q * exp10 (r - r') - q', r')
+    fun bin2dec d =
+      if 0 <= d then
+        (exp2 d, 0)
+      else
+        (exp5 (~ d), d)
+
+    val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
+    val L1 = L + 1
+
+    val (q1, r1) = subtract (q, r) (bin2dec L1) 
+  in
+    if 0 <= q1 then
+      let
+        val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
+      in
+        if 0 <= q2 then
+          raise (Floating_point "find_most_significant")
+        else
+          (L1, (q1, r1))
+      end
+    else
+      let
+        val (q0, r0) = subtract (q, r) (bin2dec L)
+      in
+        if 0 <= q0 then
+          (L, (q0, r0))
+        else
+          raise (Floating_point "find_most_significant")
+      end
+  end
+
+fun approx_dec_by_bin n (q,r) =
+  let
+    fun addseq acc d' [] = acc
+      | addseq acc d' (d::ds) = addseq (acc + exp2 (d - d')) d' ds
+
+    fun seq2bin [] = (0, 0)
+      | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
+
+    fun approx d_seq d0 precision (q,r) =
+      if q = 0 then
+        let val x = seq2bin d_seq in
+          (x, x)
+        end
+      else
+        let
+          val (d, (q', r')) = find_most_significant q r
+        in
+          if precision < d0 - d then
+            let
+              val d' = d0 - precision
+              val x1 = seq2bin (d_seq)
+              val x2 = (fst x1 * exp2 (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
+            in
+              (x1, x2)
+            end
+          else
+            approx (d::d_seq) d0 precision (q', r')
+        end
+
+    fun approx_start precision (q, r) =
+      if q = 0 then
+        ((0, 0), (0, 0))
+      else
+        let
+          val (d, (q', r')) = find_most_significant q r
+        in
+          if precision <= 0 then
+            let
+              val x1 = seq2bin [d]
+            in
+              if q' = 0 then
+                (x1, x1)
+              else
+                (x1, seq2bin [d + 1])
+            end
+          else
+            approx [d] d precision (q', r')
+        end
+  in
+    if 0 <= q then
+      approx_start n (q,r)
+    else
+      let
+        val ((a1,b1), (a2, b2)) = approx_start n (~ q, r)
+      in
+        ((~ a2, b2), (~ a1, b1))
+      end
+  end
+
+fun approx_decstr_by_bin n decstr =
+  let
+    fun str2int s = the_default 0 (Int.fromString s)
+    fun signint p x = if p then x else ~ x
+
+    val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
+    val s = size d2
+
+    val q = signint p (str2int d1 * exp10 s + str2int d2)
+    val r = signint ep (str2int e) - s
+  in
+    approx_dec_by_bin n (q,r)
+  end
+
+fun mk_float (a, b) = @{term "float"} $
+  HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
+
+fun dest_float (Const (@{const_name float}, _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
+      pairself (snd o HOLogic.dest_number) (a, b)
+  | dest_float t = ((snd o HOLogic.dest_number) t, 0);
+
+fun approx_float prec f value =
+  let
+    val interval = approx_decstr_by_bin prec value
+    val (flower, fupper) = f interval
+  in
+    (mk_float flower, mk_float fupper)
+  end;
+
+end;
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/NSA/StarDef.thy	Sat Mar 22 22:00:26 2014 +0100
@@ -172,7 +172,7 @@
   "Standard = range star_of"
 
 text {* Transfer tactic should remove occurrences of @{term star_of} *}
-setup {* Transfer_Principle.add_const "StarDef.star_of" *}
+setup {* Transfer_Principle.add_const @{const_name star_of} *}
 
 declare star_of_def [transfer_intro]
 
@@ -199,7 +199,7 @@
     UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
 
 text {* Transfer tactic should remove occurrences of @{term Ifun} *}
-setup {* Transfer_Principle.add_const "StarDef.Ifun" *}
+setup {* Transfer_Principle.add_const @{const_name Ifun} *}
 
 lemma transfer_Ifun [transfer_intro]:
   "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
@@ -306,7 +306,7 @@
 by (simp add: unstar_def star_of_inject)
 
 text {* Transfer tactic should remove occurrences of @{term unstar} *}
-setup {* Transfer_Principle.add_const "StarDef.unstar" *}
+setup {* Transfer_Principle.add_const @{const_name unstar} *}
 
 lemma transfer_unstar [transfer_intro]:
   "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
@@ -348,7 +348,7 @@
 by (simp add: Iset_def starP2_star_n)
 
 text {* Transfer tactic should remove occurrences of @{term Iset} *}
-setup {* Transfer_Principle.add_const "StarDef.Iset" *}
+setup {* Transfer_Principle.add_const @{const_name Iset} *}
 
 lemma transfer_mem [transfer_intro]:
   "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/NSA/transfer.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -35,7 +35,7 @@
     consts = Library.merge (op =) (consts1, consts2)};
 );
 
-fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
+fun unstar_typ (Type (@{type_name star}, [t])) = unstar_typ t
   | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
   | unstar_typ T = T
 
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -86,7 +86,7 @@
 
 fun mk_Cons x xs =
   let val T = fastype_of x
-  in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
+  in Const (@{const_name Cons}, T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
 
 fun add_thms_string args = Global_Theory.add_thms ((map o apfst o apfst) Binding.name args);
 fun add_thmss_string args = Global_Theory.add_thmss ((map o apfst o apfst) Binding.name args);
@@ -142,7 +142,7 @@
   
               val stmnt3 = HOLogic.mk_Trueprop
                            (HOLogic.mk_not
-                              (Const ("Finite_Set.finite", HOLogic.mk_setT ak_type --> HOLogic.boolT) $
+                              (Const (@{const_name finite}, HOLogic.mk_setT ak_type --> HOLogic.boolT) $
                                   HOLogic.mk_UNIV ak_type))
              
               val simp2 = [@{thm image_def},@{thm bex_UNIV}]@inject_thm
@@ -179,9 +179,9 @@
         val b = Free ("b", T);
         val c = Free ("c", T);
         val ab = Free ("ab", HOLogic.mk_prodT (T, T))
-        val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);
+        val cif = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
         val cswap_akname = Const (full_swap_name, swapT);
-        val cswap = Const ("Nominal.swap", swapT)
+        val cswap = Const (@{const_name Nominal.swap}, swapT)
 
         val name = swap_name ^ "_def";
         val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -215,7 +215,7 @@
         val xs = Free ("xs", mk_permT T);
         val a  = Free ("a", T) ;
 
-        val cnil  = Const ("List.list.Nil", mk_permT T);
+        val cnil  = Const (@{const_name Nil}, mk_permT T);
         
         val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (prm $ cnil $ a, a));
 
@@ -245,7 +245,7 @@
           val perm_def_name = ak_name ^ "_prm_" ^ ak_name';
           val pi = Free ("pi", mk_permT T);
           val a  = Free ("a", T');
-          val cperm = Const ("Nominal.perm", mk_permT T --> T' --> T');
+          val cperm = Const (@{const_name Nominal.perm}, mk_permT T --> T' --> T');
           val thy'' = Sign.add_path "rec" thy'
           val cperm_def = Const (Sign.full_bname thy'' perm_def_name, mk_permT T --> T' --> T');
           val thy''' = Sign.parent_path thy'';
@@ -265,7 +265,7 @@
       let
         val ak_name_qu = Sign.full_bname thy5 (ak_name);
         val i_type = Type(ak_name_qu,[]);
-        val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
+        val cat = Const (@{const_name Nominal.at}, Term.itselfT i_type --> HOLogic.boolT);
         val at_type = Logic.mk_type i_type;
         fun proof ctxt =
           simp_tac (put_simpset HOL_ss ctxt
@@ -290,14 +290,14 @@
      val (pt_ax_classes,thy7) =  fold_map (fn (ak_name, T) => fn thy =>
       let 
           val cl_name = "pt_"^ak_name;
-          val ty = TFree("'a",["HOL.type"]);
+          val ty = TFree("'a", @{sort type});
           val x   = Free ("x", ty);
           val pi1 = Free ("pi1", mk_permT T);
           val pi2 = Free ("pi2", mk_permT T);
-          val cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
-          val cnil  = Const ("List.list.Nil", mk_permT T);
-          val cappend = Const ("List.append",mk_permT T --> mk_permT T --> mk_permT T);
-          val cprm_eq = Const ("Nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
+          val cperm = Const (@{const_name Nominal.perm}, mk_permT T --> ty --> ty);
+          val cnil  = Const (@{const_name Nil}, mk_permT T);
+          val cappend = Const (@{const_name append}, mk_permT T --> mk_permT T --> mk_permT T);
+          val cprm_eq = Const (@{const_name Nominal.prm_eq}, mk_permT T --> mk_permT T --> HOLogic.boolT);
           (* nil axiom *)
           val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 
                        (cperm $ cnil $ x, x));
@@ -309,7 +309,7 @@
                        (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
                         HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
       in
-          Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
+          Axclass.define_class (Binding.name cl_name, @{sort type}) []
                 [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
                  ((Binding.name (cl_name ^ "2"), []), [axiom2]),                           
                  ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
@@ -326,7 +326,8 @@
         val pt_name_qu = Sign.full_bname thy7 ("pt_"^ak_name);
         val i_type1 = TFree("'x",[pt_name_qu]);
         val i_type2 = Type(ak_name_qu,[]);
-        val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
+        val cpt =
+          Const (@{const_name Nominal.pt}, (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
         val pt_type = Logic.mk_type i_type1;
         val at_type = Logic.mk_type i_type2;
         fun proof ctxt =
@@ -349,10 +350,10 @@
        let 
           val cl_name = "fs_"^ak_name;
           val pt_name = Sign.full_bname thy ("pt_"^ak_name);
-          val ty = TFree("'a",["HOL.type"]);
+          val ty = TFree("'a",@{sort type});
           val x   = Free ("x", ty);
-          val csupp    = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
-          val cfinite  = Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT)
+          val csupp    = Const (@{const_name Nominal.supp}, ty --> HOLogic.mk_setT T);
+          val cfinite  = Const (@{const_name finite}, HOLogic.mk_setT T --> HOLogic.boolT)
           
           val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
 
@@ -372,7 +373,7 @@
          val fs_name_qu = Sign.full_bname thy11 ("fs_"^ak_name);
          val i_type1 = TFree("'x",[fs_name_qu]);
          val i_type2 = Type(ak_name_qu,[]);
-         val cfs = Const ("Nominal.fs", 
+         val cfs = Const (@{const_name Nominal.fs},
                                  (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
          val fs_type = Logic.mk_type i_type1;
          val at_type = Logic.mk_type i_type2;
@@ -394,19 +395,19 @@
          fold_map (fn (ak_name', T') => fn thy' =>
              let
                val cl_name = "cp_"^ak_name^"_"^ak_name';
-               val ty = TFree("'a",["HOL.type"]);
+               val ty = TFree("'a",@{sort type});
                val x   = Free ("x", ty);
                val pi1 = Free ("pi1", mk_permT T);
                val pi2 = Free ("pi2", mk_permT T');                  
-               val cperm1 = Const ("Nominal.perm", mk_permT T  --> ty --> ty);
-               val cperm2 = Const ("Nominal.perm", mk_permT T' --> ty --> ty);
-               val cperm3 = Const ("Nominal.perm", mk_permT T  --> mk_permT T' --> mk_permT T');
+               val cperm1 = Const (@{const_name Nominal.perm}, mk_permT T  --> ty --> ty);
+               val cperm2 = Const (@{const_name Nominal.perm}, mk_permT T' --> ty --> ty);
+               val cperm3 = Const (@{const_name Nominal.perm}, mk_permT T  --> mk_permT T' --> mk_permT T');
 
                val ax1   = HOLogic.mk_Trueprop 
                            (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
                                            cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
                in  
-                 Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
+                 Axclass.define_class (Binding.name cl_name, @{sort type}) []
                    [((Binding.name (cl_name ^ "1"), []), [ax1])] thy'  
                end) ak_names_types thy) ak_names_types thy12;
 
@@ -422,7 +423,7 @@
              val i_type0 = TFree("'a",[cp_name_qu]);
              val i_type1 = Type(ak_name_qu,[]);
              val i_type2 = Type(ak_name_qu',[]);
-             val ccp = Const ("Nominal.cp",
+             val ccp = Const (@{const_name Nominal.cp},
                              (Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
                                                       (Term.itselfT i_type2)-->HOLogic.boolT);
              val at_type  = Logic.mk_type i_type1;
@@ -456,7 +457,7 @@
                  val ak_name_qu' = Sign.full_bname thy' ak_name';
                  val i_type1 = Type(ak_name_qu,[]);
                  val i_type2 = Type(ak_name_qu',[]);
-                 val cdj = Const ("Nominal.disjoint",
+                 val cdj = Const (@{const_name Nominal.disjoint},
                            (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
                  val at_type  = Logic.mk_type i_type1;
                  val at_type' = Logic.mk_type i_type2;
@@ -548,15 +549,14 @@
           val pt_thm_unit  = pt_unit_inst;
        in
         thy
-        |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
-        |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
-        |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
-        |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
-        |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
-        |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
-        |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
-                                    (pt_proof pt_thm_nprod)
-        |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
+        |> Axclass.prove_arity (@{type_name fun},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
+        |> Axclass.prove_arity (@{type_name set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
+        |> Axclass.prove_arity (@{type_name noption},[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
+        |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
+        |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
+        |> Axclass.prove_arity (@{type_name prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
+        |> Axclass.prove_arity (@{type_name nprod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_nprod)
+        |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (pt_proof pt_thm_unit)
      end) ak_names thy13; 
 
        (********  fs_<ak> class instances  ********)
@@ -614,12 +614,11 @@
           val fs_thm_optn  = fs_inst RS fs_option_inst;
         in 
          thy
-         |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
-         |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
-         |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
-                                     (fs_proof fs_thm_nprod) 
-         |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
-         |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
+         |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (fs_proof fs_thm_unit) 
+         |> Axclass.prove_arity (@{type_name prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
+         |> Axclass.prove_arity (@{type_name nprod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_nprod)
+         |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
+         |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
         end) ak_names thy20;
 
        (********  cp_<ak>_<ai> class instances  ********)
@@ -698,13 +697,13 @@
             val cp_thm_set = cp_inst RS cp_set_inst;
         in
          thy'
-         |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
+         |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (cp_proof cp_thm_unit)
          |> Axclass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
-         |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
-         |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
-         |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
-         |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
-         |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
+         |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
+         |> Axclass.prove_arity (@{type_name fun},[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
+         |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
+         |> Axclass.prove_arity (@{type_name noption},[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
+         |> Axclass.prove_arity (@{type_name set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
         end) ak_names thy) ak_names thy25;
 
      (* show that discrete nominal types are permutation types, finitely     *)
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -90,13 +90,14 @@
 
 val dj_cp = @{thm dj_cp};
 
-fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]),
-      Type ("fun", [_, U])])) = (T, U);
+fun dest_permT (Type (@{type_name fun},
+    [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [T, _])]),
+      Type (@{type_name fun}, [_, U])])) = (T, U);
 
-fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
+fun permTs_of (Const (@{const_name Nominal.perm}, T) $ t $ u) = fst (dest_permT T) :: permTs_of u
   | permTs_of _ = [];
 
-fun perm_simproc' ctxt (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
+fun perm_simproc' ctxt (Const (@{const_name Nominal.perm}, T) $ t $ (u as Const (@{const_name Nominal.perm}, U) $ r $ s)) =
       let
         val thy = Proof_Context.theory_of ctxt;
         val (aT as Type (a, []), S) = dest_permT T;
@@ -140,23 +141,23 @@
   let
     val T = fastype_of1 (Ts, t);
     val U = fastype_of1 (Ts, u)
-  in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
+  in Const (@{const_name Nominal.perm}, T --> U --> U) $ t $ u end;
 
 fun perm_of_pair (x, y) =
   let
     val T = fastype_of x;
     val pT = mk_permT T
-  in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
-    HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
+  in Const (@{const_name Cons}, HOLogic.mk_prodT (T, T) --> pT --> pT) $
+    HOLogic.mk_prod (x, y) $ Const (@{const_name Nil}, pT)
   end;
 
 fun mk_not_sym ths = maps (fn th => case prop_of th of
     _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
   | _ => [th]) ths;
 
-fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
+fun fresh_const T U = Const (@{const_name Nominal.fresh}, T --> U --> HOLogic.boolT);
 fun fresh_star_const T U =
-  Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
+  Const (@{const_name Nominal.fresh_star}, HOLogic.mk_setT T --> U --> HOLogic.boolT);
 
 fun gen_nominal_datatype prep_specs config dts thy =
   let
@@ -185,8 +186,8 @@
       (Sign.full_name thy n, Sign.full_name thy (Binding.suffix_name "_Rep" n))) dts;
     val rps = map Library.swap ps;
 
-    fun replace_types (Type ("Nominal.ABS", [T, U])) =
-          Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
+    fun replace_types (Type (@{type_name ABS}, [T, U])) =
+          Type (@{type_name fun}, [T, Type (@{type_name noption}, [replace_types U])])
       | replace_types (Type (s, Ts)) =
           Type (the_default s (AList.lookup op = ps s), map replace_types Ts)
       | replace_types T = T;
@@ -208,14 +209,14 @@
 
     (**** define permutation functions ****)
 
-    val permT = mk_permT (TFree ("'x", HOLogic.typeS));
+    val permT = mk_permT (TFree ("'x", @{sort type}));
     val pi = Free ("pi", permT);
     val perm_types = map (fn (i, _) =>
       let val T = nth_dtyp i
       in permT --> T --> T end) descr;
     val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
       "perm_" ^ Datatype_Aux.name_of_typ (nth_dtyp i)) descr);
-    val perm_names = replicate (length new_type_names) "Nominal.perm" @
+    val perm_names = replicate (length new_type_names) @{const_name Nominal.perm} @
       map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
     val perm_names_types = perm_names ~~ perm_types;
     val perm_names_types' = perm_names' ~~ perm_types;
@@ -236,16 +237,16 @@
                   fold_rev (Term.abs o pair "x") Us
                     (Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
                       list_comb (x, map (fn (i, U) =>
-                        Const ("Nominal.perm", permT --> U --> U) $
-                          (Const ("List.rev", permT --> permT) $ pi) $
+                        Const (@{const_name Nominal.perm}, permT --> U --> U) $
+                          (Const (@{const_name rev}, permT --> permT) $ pi) $
                           Bound i) ((length Us - 1 downto 0) ~~ Us)))
                 end
-              else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
+              else Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x
             end;
         in
           (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
             (Free (nth perm_names_types' i) $
-               Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
+               Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
                list_comb (c, args),
              list_comb (c, map perm_arg (dts ~~ args)))))
         end) constrs
@@ -274,7 +275,7 @@
             (map (fn (c as (s, T), x) =>
                let val [T1, T2] = binder_types T
                in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
-                 Const ("Nominal.perm", T) $ pi $ Free (x, T2))
+                 Const (@{const_name Nominal.perm}, T) $ pi $ Free (x, T2))
                end)
              (perm_names_types ~~ perm_indnames))))
           (fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
@@ -293,7 +294,7 @@
             (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
               (map (fn ((s, T), x) => HOLogic.mk_eq
                   (Const (s, permT --> T --> T) $
-                     Const ("List.list.Nil", permT) $ Free (x, T),
+                     Const (@{const_name Nil}, permT) $ Free (x, T),
                    Free (x, T)))
                (perm_names ~~
                 map body_type perm_types ~~ perm_indnames)))))
@@ -326,7 +327,7 @@
                 (map (fn ((s, T), x) =>
                     let val perm = Const (s, permT --> T --> T)
                     in HOLogic.mk_eq
-                      (perm $ (Const ("List.append", permT --> permT --> permT) $
+                      (perm $ (Const (@{const_name append}, permT --> permT --> permT) $
                          pi1 $ pi2) $ Free (x, T),
                        perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
                     end)
@@ -357,7 +358,7 @@
       in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm
         (Goal.prove_global_future thy2 [] []
           (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
-             (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
+             (HOLogic.mk_Trueprop (Const (@{const_name Nominal.prm_eq},
                 permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
               HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
                 (map (fn ((s, T), x) =>
@@ -414,7 +415,7 @@
                     val pi2 = Free ("pi2", permT2);
                     val perm1 = Const (s, permT1 --> T --> T);
                     val perm2 = Const (s, permT2 --> T --> T);
-                    val perm3 = Const ("Nominal.perm", permT1 --> permT2 --> permT2)
+                    val perm3 = Const (@{const_name Nominal.perm}, permT1 --> permT2 --> permT2)
                   in HOLogic.mk_eq
                     (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
                      perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
@@ -462,17 +463,17 @@
         (map (fn (i, _) => Datatype_Aux.name_of_typ (nth_dtyp i) ^ "_set") descr);
     val big_rep_name =
       space_implode "_" (Datatype_Prop.indexify_names (map_filter
-        (fn (i, ("Nominal.noption", _, _)) => NONE
+        (fn (i, (@{type_name noption}, _, _)) => NONE
           | (i, _) => SOME (Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set";
     val _ = warning ("big_rep_name: " ^ big_rep_name);
 
     fun strip_option (dtf as Datatype.DtType ("fun", [dt, Datatype.DtRec i])) =
           (case AList.lookup op = descr i of
-             SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
+             SOME (@{type_name noption}, _, [(_, [dt']), _]) =>
                apfst (cons dt) (strip_option dt')
            | _ => ([], dtf))
       | strip_option (Datatype.DtType ("fun",
-            [dt, Datatype.DtType ("Nominal.noption", [dt'])])) =
+            [dt, Datatype.DtType (@{type_name noption}, [dt'])])) =
           apfst (cons dt) (strip_option dt')
       | strip_option dt = ([], dt);
 
@@ -493,8 +494,8 @@
             val free' = Datatype_Aux.app_bnds free (length Us);
             fun mk_abs_fun T (i, t) =
               let val U = fastype_of t
-              in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
-                Type ("Nominal.noption", [U])) $ Datatype_Aux.mk_Free "y" T i $ t)
+              in (i + 1, Const (@{const_name Nominal.abs_fun}, [T, U, T] --->
+                Type (@{type_name noption}, [U])) $ Datatype_Aux.mk_Free "y" T i $ t)
               end
           in (j + 1, j' + length Ts,
             case dt'' of
@@ -513,7 +514,7 @@
 
     val (intr_ts, (rep_set_names', recTs')) =
       apfst flat (apsnd ListPair.unzip (ListPair.unzip (map_filter
-        (fn ((_, ("Nominal.noption", _, _)), _) => NONE
+        (fn ((_, (@{type_name noption}, _, _)), _) => NONE
           | ((i, (_, _, constrs)), rep_set_name) =>
               let val T = nth_dtyp i
               in SOME (map (make_intr rep_set_name T) constrs,
@@ -540,7 +541,7 @@
     val abs_perm = Global_Theory.get_thms thy4 "abs_perm";
 
     val perm_indnames' = map_filter
-      (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
+      (fn (x, (_, (@{type_name noption}, _, _))) => NONE | (x, _) => SOME x)
       (perm_indnames ~~ descr);
 
     fun mk_perm_closed name = map (fn th => Drule.export_without_context (th RS mp))
@@ -553,7 +554,7 @@
                  val S = Const (s, T --> HOLogic.boolT);
                  val permT = mk_permT (Type (name, []))
                in HOLogic.mk_imp (S $ Free (x, T),
-                 S $ (Const ("Nominal.perm", permT --> T --> T) $
+                 S $ (Const (@{const_name Nominal.perm}, permT --> T --> T) $
                    Free ("pi", permT) $ Free (x, T)))
                end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
         (fn {context = ctxt, ...} => EVERY
@@ -581,15 +582,15 @@
               (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
         let
           val permT = mk_permT
-            (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
+            (TFree (singleton (Name.variant_list (map fst tvs)) "'a", @{sort type}));
           val pi = Free ("pi", permT);
           val T = Type (Sign.full_name thy name, map TFree tvs);
         in apfst (pair r o hd)
           (Global_Theory.add_defs_unchecked true
             [((Binding.map_name (fn n => "prm_" ^ n ^ "_def") name, Logic.mk_equals
-              (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
+              (Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ Free ("x", T),
                Const (Sign.intern_const thy ("Abs_" ^ Binding.name_of name), U --> T) $
-                 (Const ("Nominal.perm", permT --> U --> U) $ pi $
+                 (Const (@{const_name Nominal.perm}, permT --> U --> U) $ pi $
                    (Const (Sign.intern_const thy ("Rep_" ^ Binding.name_of name), T --> U) $
                      Free ("x", T))))), [])] thy)
         end))
@@ -671,12 +672,12 @@
         val T = fastype_of x;
         val U = fastype_of t
       in
-        Const ("Nominal.abs_fun", T --> U --> T -->
-          Type ("Nominal.noption", [U])) $ x $ t
+        Const (@{const_name Nominal.abs_fun}, T --> U --> T -->
+          Type (@{type_name noption}, [U])) $ x $ t
       end;
 
     val (ty_idxs, _) = List.foldl
-      (fn ((i, ("Nominal.noption", _, _)), p) => p
+      (fn ((i, (@{type_name noption}, _, _)), p) => p
         | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
 
     fun reindex (Datatype.DtType (s, dts)) = Datatype.DtType (s, map reindex dts)
@@ -691,7 +692,7 @@
       in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
 
     val (descr'', ndescr) = ListPair.unzip (map_filter
-      (fn (i, ("Nominal.noption", _, _)) => NONE
+      (fn (i, (@{type_name noption}, _, _)) => NONE
         | (i, (s, dts, constrs)) =>
              let
                val SOME index = AList.lookup op = ty_idxs i;
@@ -817,8 +818,8 @@
           (augment_sort thy8
             (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
             (HOLogic.mk_Trueprop (HOLogic.mk_eq
-              (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
-               Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
+              (Const (@{const_name Nominal.perm}, permT --> U --> U) $ pi $ (Rep $ x),
+               Rep $ (Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x)))))
           (fn {context = ctxt, ...} =>
             simp_tac (put_simpset HOL_basic_ss ctxt addsimps (perm_defs @ Abs_inverse_thms @
             perm_closed_thms @ Rep_thms)) 1)
@@ -860,7 +861,7 @@
 
           fun perm t =
             let val T = fastype_of t
-            in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
+            in Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ t end;
 
           fun constr_arg (dts, dt) (j, l_args, r_args) =
             let
@@ -977,7 +978,7 @@
           val Ts = map fastype_of args1;
           val c = list_comb (Const (cname, Ts ---> T), args1);
           fun supp t =
-            Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
+            Const (@{const_name Nominal.supp}, fastype_of t --> HOLogic.mk_setT atomT) $ t;
           fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t;
           val supp_thm = Goal.prove_global_future thy8 [] []
             (augment_sort thy8 pt_cp_sort
@@ -1070,8 +1071,8 @@
            (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
              (HOLogic.mk_Trueprop
                (foldr1 HOLogic.mk_conj (map (fn (s, T) =>
-                 Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
-                   (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
+                 Const (@{const_name finite}, HOLogic.mk_setT atomT --> HOLogic.boolT) $
+                   (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT atomT) $ Free (s, T)))
                    (indnames ~~ recTs)))))
            (fn {context = ctxt, ...} => Datatype_Aux.ind_tac dt_induct indnames 1 THEN
             ALLGOALS (asm_full_simp_tac (ctxt addsimps
@@ -1112,10 +1113,10 @@
 
     val pnames = if length descr'' = 1 then ["P"]
       else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
-    val ind_sort = if null dt_atomTs then HOLogic.typeS
+    val ind_sort = if null dt_atomTs then @{sort type}
       else Sign.minimize_sort thy9 (Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms));
     val fsT = TFree ("'n", ind_sort);
-    val fsT' = TFree ("'n", HOLogic.typeS);
+    val fsT' = TFree ("'n", @{sort type});
 
     val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
       (Datatype_Prop.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
@@ -1183,7 +1184,7 @@
 
     val ind_prems' =
       map (fn (_, f as Free (_, T)) => Logic.all (Free ("x", fsT'))
-        (HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
+        (HOLogic.mk_Trueprop (Const (@{const_name finite},
           Term.range_type T -->
             HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
       maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
@@ -1345,7 +1346,7 @@
                           cut_facts_tac iprems 1,
                           (resolve_tac prems THEN_ALL_NEW
                             SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
-                                _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
+                                _ $ (Const (@{const_name Nominal.fresh}, _) $ _ $ _) =>
                                   simp_tac ind_ss1' i
                               | _ $ (Const (@{const_name Not}, _) $ _) =>
                                   resolve_tac freshs2' i
@@ -1371,7 +1372,7 @@
       map (fn (_, f) =>
         let val f' = Logic.varify_global f
         in (cterm_of thy9 f',
-          cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
+          cterm_of thy9 (Const (@{const_name Nominal.supp}, fastype_of f')))
         end) fresh_fs) induct_aux;
 
     val induct = Goal.prove_global_future thy9 []
@@ -1398,7 +1399,7 @@
 
     val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' used;
 
-    val rec_sort = if null dt_atomTs then HOLogic.typeS else
+    val rec_sort = if null dt_atomTs then @{sort type} else
       Sign.minimize_sort thy10 (Sign.certify_sort thy10 pt_cp_sort);
 
     val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
@@ -1459,8 +1460,8 @@
           HOLogic.mk_Trueprop (nth rec_preds i $ Free y)) (recs ~~ frees'');
         val prems5 = mk_fresh3 (recs ~~ frees'') frees';
         val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
-          (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
-             (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y)))
+          (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
+             (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT aT) $ Free y)))
                frees'') atomTs;
         val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop
           (fresh_const T fsT' $ Free x $ rec_ctxt)) binders;
@@ -1534,7 +1535,7 @@
               (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
             (fn {context = ctxt, ...} => dtac (Thm.instantiate ([],
                  [(cterm_of thy11 (Var (("pi", 0), permT)),
-                   cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN
+                   cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN
                NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths)
       in (ths, ths') end) dt_atomTs);
 
@@ -1545,9 +1546,9 @@
         val name = Long_Name.base_name (fst (dest_Type aT));
         val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
         val aset = HOLogic.mk_setT aT;
-        val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
+        val finite = Const (@{const_name finite}, aset --> HOLogic.boolT);
         val fins = map (fn (f, T) => HOLogic.mk_Trueprop
-          (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
+          (finite $ (Const (@{const_name Nominal.supp}, T --> aset) $ f)))
             (rec_fns ~~ rec_fn_Ts)
       in
         map (fn th => Drule.export_without_context (th RS mp)) (Datatype_Aux.split_conj_thm
@@ -1561,7 +1562,7 @@
                      val y = Free ("y" ^ string_of_int i, U)
                    in
                      HOLogic.mk_imp (R $ x $ y,
-                       finite $ (Const ("Nominal.supp", U --> aset) $ y))
+                       finite $ (Const (@{const_name Nominal.supp}, U --> aset) $ y))
                    end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~
                      (1 upto length recTs))))))
             (fn {prems = fins, context = ctxt} =>
@@ -1573,8 +1574,8 @@
 
     val finite_premss = map (fn aT =>
       map (fn (f, T) => HOLogic.mk_Trueprop
-        (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
-           (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f)))
+        (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
+           (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT aT) $ f)))
            (rec_fns ~~ rec_fn_Ts)) dt_atomTs;
 
     val rec_fns' = map (augment_sort thy11 fs_cp_sort) rec_fns;
@@ -1613,7 +1614,7 @@
                  in EVERY
                    [rtac (Drule.cterm_instantiate
                       [(cterm_of thy11 S,
-                        cterm_of thy11 (Const ("Nominal.supp",
+                        cterm_of thy11 (Const (@{const_name Nominal.supp},
                           fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
                       supports_fresh) 1,
                     simp_tac (put_simpset HOL_basic_ss context addsimps
@@ -1654,7 +1655,7 @@
     val induct_aux_rec = Drule.cterm_instantiate
       (map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
          (map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT,
-            Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
+            Const (@{const_name Nominal.supp}, fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
               fresh_fs @
           map (fn (((P, T), (x, U)), Q) =>
            (Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)),
@@ -1684,8 +1685,8 @@
 
     val finite_ctxt_prems = map (fn aT =>
       HOLogic.mk_Trueprop
-        (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
-           (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
+        (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
+           (Const (@{const_name Nominal.supp}, fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
 
     val rec_unique_thms = Datatype_Aux.split_conj_thm (Goal.prove
       (Proof_Context.init_global thy11) (map fst rec_unique_frees)
@@ -1752,7 +1753,7 @@
                         | _ => false)
                       | _ => false) prems';
                     val fresh_prems = filter (fn th => case prop_of th of
-                        _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
+                        _ $ (Const (@{const_name Nominal.fresh}, _) $ _ $ _) => true
                       | _ $ (Const (@{const_name Not}, _) $ _) => true
                       | _ => false) prems';
                     val Ts = map fastype_of boundsl;
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -87,8 +87,8 @@
   | get_inner_fresh_fun (v as Var _)  = NONE
   | get_inner_fresh_fun (Const _) = NONE
   | get_inner_fresh_fun (Abs (_, _, t)) = get_inner_fresh_fun t
-  | get_inner_fresh_fun (Const ("Nominal.fresh_fun",Type("fun",[Type ("fun",[Type (T,_),_]),_])) $ u)
-                           = SOME T
+  | get_inner_fresh_fun (Const (@{const_name Nominal.fresh_fun},
+      Type(@{type_name fun},[Type (@{type_name fun},[Type (T,_),_]),_])) $ u) = SOME T
   | get_inner_fresh_fun (t $ u) =
      let val a = get_inner_fresh_fun u in
      if a = NONE then get_inner_fresh_fun t else a
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -196,7 +196,7 @@
       end) (Logic.strip_imp_prems raw_induct' ~~ avoids');
 
     val atomTs = distinct op = (maps (map snd o #2) prems);
-    val ind_sort = if null atomTs then HOLogic.typeS
+    val ind_sort = if null atomTs then @{sort type}
       else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
         ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
     val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
@@ -332,7 +332,7 @@
                  fun concat_perm pi1 pi2 =
                    let val T = fastype_of pi1
                    in if T = fastype_of pi2 then
-                       Const (@{const_name List.append}, T --> T --> T) $ pi1 $ pi2
+                       Const (@{const_name append}, T --> T --> T) $ pi1 $ pi2
                      else pi2
                    end;
                  val pis'' = fold (concat_perm #> map) pis' pis;
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -45,7 +45,7 @@
 
 fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
   (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
-    fn Const ("Nominal.perm", _) $ _ $ t =>
+    fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
          then SOME perm_bool else NONE
      | _ => NONE);
@@ -97,13 +97,13 @@
       (case head_of p of
          Const (name, _) =>
            if member (op =) names name then SOME (HOLogic.mk_conj (p,
-             Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
+             Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
                (subst_bounds (pis, strip_all pis q))))
            else NONE
        | _ => NONE)
   | inst_conj_all names ps pis t u =
       if member (op aconv) ps (head_of u) then
-        SOME (Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
+        SOME (Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
           (subst_bounds (pis, strip_all pis t)))
       else NONE
   | inst_conj_all _ _ _ _ _ = NONE;
@@ -222,7 +222,7 @@
 
     val atomTs = distinct op = (maps (map snd o #2) prems);
     val atoms = map (fst o dest_Type) atomTs;
-    val ind_sort = if null atomTs then HOLogic.typeS
+    val ind_sort = if null atomTs then @{sort type}
       else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
         ("fs_" ^ Long_Name.base_name a)) atoms));
     val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
@@ -292,7 +292,7 @@
       ("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
     val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
       addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
-      addsimprocs [mk_perm_bool_simproc ["Fun.id"],
+      addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}],
         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
     val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
     val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
@@ -312,7 +312,7 @@
         (** protect terms to avoid that fresh_star_prod_set interferes with  **)
         (** pairs used in introduction rules of inductive predicate          **)
         fun protect t =
-          let val T = fastype_of t in Const ("Fun.id", T --> T) $ t end;
+          let val T = fastype_of t in Const (@{const_name Fun.id}, T --> T) $ t end;
         val p = foldr1 HOLogic.mk_prod (map protect ts);
         val atom = fst (dest_Type T);
         val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
@@ -393,7 +393,7 @@
                  fun concat_perm pi1 pi2 =
                    let val T = fastype_of pi1
                    in if T = fastype_of pi2 then
-                       Const ("List.append", T --> T --> T) $ pi1 $ pi2
+                       Const (@{const_name append}, T --> T --> T) $ pi1 $ pi2
                      else pi2
                    end;
                  val pis'' = fold_rev (concat_perm #> map) pis' pis;
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -97,14 +97,15 @@
     (* constant or when (f x) is a permuation with two or more arguments     *)
     fun applicable_app t = 
           (case (strip_comb t) of
-              (Const ("Nominal.perm",_),ts) => (length ts) >= 2
+              (Const (@{const_name Nominal.perm},_),ts) => (length ts) >= 2
             | (Const _,_) => false
             | _ => true)
   in
     case redex of 
         (* case pi o (f x) == (pi o f) (pi o x)          *)
-        (Const("Nominal.perm",
-          Type("fun",[Type("List.list",[Type(@{type_name Product_Type.prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
+        (Const(@{const_name Nominal.perm},
+          Type(@{type_name fun},
+            [Type(@{type_name list}, [Type(@{type_name prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
             (if (applicable_app f) then
               let
                 val name = Long_Name.base_name n
@@ -124,13 +125,13 @@
      fun applicable_fun t =
        (case (strip_comb t) of
           (Abs _ ,[]) => true
-        | (Const ("Nominal.perm",_),_) => false
+        | (Const (@{const_name Nominal.perm},_),_) => false
         | (Const _, _) => true
         | _ => false)
    in
      case redex of 
        (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
-       (Const("Nominal.perm",_) $ pi $ f)  => 
+       (Const(@{const_name Nominal.perm},_) $ pi $ f)  => 
           (if applicable_fun f then SOME perm_fun_def else NONE)
       | _ => NONE
    end
@@ -190,9 +191,9 @@
 
 fun perm_compose_simproc' ctxt redex =
   (case redex of
-     (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
-       [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
-         Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ 
+     (Const (@{const_name Nominal.perm}, Type (@{type_name fun}, [Type (@{type_name list},
+       [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (@{const_name Nominal.perm}, 
+         Type (@{type_name fun}, [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ 
           pi2 $ t)) =>
     let
       val thy = Proof_Context.theory_of ctxt
@@ -293,7 +294,7 @@
     let val goal = nth (cprems_of st) (i - 1)
     in
       case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of
-          _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
+          _ $ (Const (@{const_name finite}, _) $ (Const (@{const_name Nominal.supp}, T) $ x)) =>
           let
             val cert = Thm.cterm_of (Thm.theory_of_thm st);
             val ps = Logic.strip_params (term_of goal);
@@ -303,7 +304,7 @@
                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
               vs HOLogic.unit;
             val s' = fold_rev Term.abs ps
-              (Const ("Nominal.supp", fastype_of1 (Ts, s) -->
+              (Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) -->
                 Term.range_type T) $ s);
             val supports_rule' = Thm.lift_rule goal supports_rule;
             val _ $ (_ $ S $ _) =
@@ -337,7 +338,7 @@
         val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
     in
       case Logic.strip_assums_concl (term_of goal) of
-          _ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => 
+          _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) => 
           let
             val cert = Thm.cterm_of (Thm.theory_of_thm st);
             val ps = Logic.strip_params (term_of goal);
@@ -348,7 +349,7 @@
               vs HOLogic.unit;
             val s' =
               fold_rev Term.abs ps
-                (Const ("Nominal.supp", fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
+                (Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
             val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
             val _ $ (_ $ S $ _) =
               Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/TLA/Action.thy	Sat Mar 22 22:00:26 2014 +0100
@@ -117,7 +117,7 @@
 
 fun action_use ctxt th =
     case (concl_of th) of
-      Const _ $ (Const ("Intensional.Valid", _) $ _) =>
+      Const _ $ (Const (@{const_name Valid}, _) $ _) =>
               (flatten (action_unlift ctxt th) handle THM _ => th)
     | _ => th;
 *}
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/TLA/Intensional.thy	Sat Mar 22 22:00:26 2014 +0100
@@ -283,7 +283,7 @@
 
 fun int_use ctxt th =
     case (concl_of th) of
-      Const _ $ (Const ("Intensional.Valid", _) $ _) =>
+      Const _ $ (Const (@{const_name Valid}, _) $ _) =>
               (flatten (int_unlift ctxt th) handle THM _ => th)
     | _ => th
 *}
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -256,11 +256,11 @@
   in
     case thf_ty of
        Prod_type (thf_ty1, thf_ty2) =>
-         Type ("Product_Type.prod",
+         Type (@{type_name prod},
           [interpret_type config thy type_map thf_ty1,
            interpret_type config thy type_map thf_ty2])
      | Fn_type (thf_ty1, thf_ty2) =>
-         Type ("fun",
+         Type (@{type_name fun},
           [interpret_type config thy type_map thf_ty1,
            interpret_type config thy type_map thf_ty2])
      | Atom_type _ =>
@@ -398,8 +398,7 @@
 (*As above, but for products*)
 fun mtimes thy =
   fold (fn x => fn y =>
-    Sign.mk_const thy
-    ("Product_Type.Pair", [dummyT, dummyT]) $ y $ x)
+    Sign.mk_const thy (@{const_name Pair}, [dummyT, dummyT]) $ y $ x)
 
 fun mtimes' (args, thy) f =
   let
@@ -456,11 +455,11 @@
   end
 
 (*Next batch of functions give info about Isabelle/HOL types*)
-fun is_fun (Type ("fun", _)) = true
+fun is_fun (Type (@{type_name fun}, _)) = true
   | is_fun _ = false
-fun is_prod (Type ("Product_Type.prod", _)) = true
+fun is_prod (Type (@{type_name prod}, _)) = true
   | is_prod _ = false
-fun dom_type (Type ("fun", [ty1, _])) = ty1
+fun dom_type (Type (@{type_name fun}, [ty1, _])) = ty1
 fun is_prod_typed thy config symb =
   let
     fun symb_type const_name =
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat Mar 22 22:00:26 2014 +0100
@@ -999,15 +999,15 @@
     val is =
       upto (1, arity)
       |> map Int.toString
-    val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)) is
-    val res_ty = TFree ("res" ^ "_ty", HOLogic.typeS)
+    val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", @{sort type})) is
+    val res_ty = TFree ("res" ^ "_ty", @{sort type})
     val f_ty = arg_tys ---> res_ty
     val f = Free ("f", f_ty)
     val xs = map (fn i =>
-      Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
+      Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
     (*FIXME DRY principle*)
     val ys = map (fn i =>
-      Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
+      Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
 
     val hyp_lhs = list_comb (f, xs)
     val hyp_rhs = list_comb (f, ys)
@@ -1018,7 +1018,7 @@
       |> HOLogic.mk_Trueprop
     fun conc_eq i =
       let
-        val ty = TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)
+        val ty = TFree ("arg" ^ i ^ "_ty", @{sort type})
         val x = Free ("x" ^ i, ty)
         val y = Free ("y" ^ i, ty)
         val eq = HOLogic.eq_const ty $ x $ y
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 22 22:00:26 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 [] []
@@ -707,7 +707,7 @@
 
 fun gen_add_datatype prep_specs config raw_specs thy =
   let
-    val _ = Theory.requires thy "Datatype" "datatype definitions";
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "datatype definitions";
 
     val (dts, spec_ctxt) = prep_specs raw_specs thy;
     val ((_, tyvars, _), _) :: _ = dts;
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -446,30 +446,35 @@
     let
       val assms = map (perhaps (try HOLogic.dest_Trueprop)) (prems_of rule)
       val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of rule);
-      val (lhs, rhs) = case concl of
-        Const ("Orderings.ord_class.less_eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs => 
-          (lhs, rhs)
-        | Const ("Orderings.ord_class.less_eq", _) $ rhs $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) => 
-          (lhs, rhs)
-        | Const ("HOL.eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs => (lhs, rhs)
-        | _ => error "The rule has a wrong format."
+      val (lhs, rhs) =
+        (case concl of
+          Const (@{const_name less_eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs =>
+            (lhs, rhs)
+        | Const (@{const_name less_eq}, _) $ rhs $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) =>
+            (lhs, rhs)
+        | Const (@{const_name HOL.eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs =>
+            (lhs, rhs)
+        | _ => error "The rule has a wrong format.")
       
       val lhs_vars = Term.add_vars lhs []
       val rhs_vars = Term.add_vars rhs []
       val assms_vars = fold Term.add_vars assms [];
-      val _ = if has_duplicates op= lhs_vars then error "Left-hand side has variable duplicates" else ()
-      val _ = if subset op= (rhs_vars, lhs_vars) then () 
+      val _ =
+        if has_duplicates op= lhs_vars
+        then error "Left-hand side has variable duplicates" else ()
+      val _ =
+        if subset op= (rhs_vars, lhs_vars) then () 
         else error "Extra variables in the right-hand side of the rule"
-      val _ = if subset op= (assms_vars, lhs_vars) then () 
+      val _ =
+        if subset op= (assms_vars, lhs_vars) then () 
         else error "Extra variables in the assumptions of the rule"
       val rhs_args = (snd o strip_comb) rhs;
-      fun check_comp t = case t of 
-        Const ("Relation.relcompp", _) $ Var (_, _) $ Var (_,_) => ()
-        | _ => error "There is an argument on the rhs that is not a composition."
+      fun check_comp t =
+        (case t of
+          Const (@{const_name relcompp}, _) $ Var _ $ Var _ => ()
+        | _ => error "There is an argument on the rhs that is not a composition.")
       val _ = map check_comp rhs_args
-    in
-      ()
-    end
+    in () end
 in
 
   fun add_distr_rule distr_rule ctxt = 
@@ -477,13 +482,13 @@
       val _ = sanity_check distr_rule
       val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of distr_rule)
     in
-      case concl of
-        Const ("Orderings.ord_class.less_eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ => 
+      (case concl of
+        Const (@{const_name less_eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ =>
           add_pos_distr_rule distr_rule ctxt
-        | Const ("Orderings.ord_class.less_eq", _) $ _ $ (Const ("Relation.relcompp",_) $ _ $ _) => 
+      | Const (@{const_name less_eq}, _) $ _ $ (Const (@{const_name relcompp},_) $ _ $ _) =>
           add_neg_distr_rule distr_rule ctxt
-        | Const ("HOL.eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ =>
-          add_eq_distr_rule distr_rule ctxt
+      | Const (@{const_name HOL.eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ =>
+          add_eq_distr_rule distr_rule ctxt)
     end
 end
 
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -85,16 +85,16 @@
   val eq_OO_meta = mk_meta_eq @{thm eq_OO} 
 
   fun print_generate_pcr_cr_eq_error ctxt term = 
-  let
-    val goal = (Const ("HOL.eq", dummyT)) $ term $ Const ("HOL.eq", dummyT)
-    val error_msg = cat_lines 
-      ["Generation of a pcr_cr_eq failed.",
-      (Pretty.string_of (Pretty.block
-         [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
-       "Most probably a relator_eq rule for one of the involved types is missing."]
-  in
-    error error_msg
-  end
+    let
+      val goal = Const (@{const_name HOL.eq}, dummyT) $ term $ Const (@{const_name HOL.eq}, dummyT)
+      val error_msg = cat_lines 
+        ["Generation of a pcr_cr_eq failed.",
+        (Pretty.string_of (Pretty.block
+           [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
+         "Most probably a relator_eq rule for one of the involved types is missing."]
+    in
+      error error_msg
+    end
 in
   fun define_pcr_cr_eq lthy pcr_rel_def =
     let
@@ -121,15 +121,15 @@
           (Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy))))
   in
     case (term_of o Thm.rhs_of) pcr_cr_eq of
-      Const (@{const_name "relcompp"}, _) $ Const ("HOL.eq", _) $ _ => 
+      Const (@{const_name "relcompp"}, _) $ Const (@{const_name HOL.eq}, _) $ _ =>
         let
           val thm = 
             pcr_cr_eq
             |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
             |> mk_HOL_eq
             |> singleton (Variable.export lthy orig_lthy)
-          val ((_, [thm]), lthy) = Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []), 
-            [thm]) lthy
+          val ((_, [thm]), lthy) =
+            Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []), [thm]) lthy
         in
           (thm, lthy)
         end
@@ -626,7 +626,7 @@
     val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def
     (**)    
     val quot_thm = case typedef_set of
-      Const ("Orderings.top_class.top", _) => 
+      Const (@{const_name top}, _) => 
         [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
       | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
         [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
@@ -638,7 +638,7 @@
     fun qualify suffix = Binding.qualified true suffix qty_name
     val opt_reflp_thm = 
       case typedef_set of
-        Const ("Orderings.top_class.top", _) => 
+        Const (@{const_name top}, _) => 
           SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
         | _ =>  NONE
     val dom_thm = get_Domainp_thm quot_thm
@@ -819,7 +819,7 @@
                     Pretty.brk 1,
                     Display.pretty_thm ctxt pcr_cr_eq]]
             val (pcr_const_eq, eqs) = strip_comb eq_lhs
-            fun is_eq (Const ("HOL.eq", _)) = true
+            fun is_eq (Const (@{const_name HOL.eq}, _)) = true
               | is_eq _ = false
             fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
               | eq_Const _ _ = false
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -176,8 +176,10 @@
         val (Ts, fns) = split_list xs
         val constr = Const (c, Ts ---> simpleT)
         val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
-        val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
-        val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
+        val Eval_App =
+          Const (@{const_name Code_Evaluation.App}, HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
+        val Eval_Const =
+          Const (@{const_name Code_Evaluation.Const}, HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
         val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
           bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
         val start_term = test_function simpleT $ 
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/TFL/usyntax.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/float_arith.ML
--- a/src/HOL/Tools/float_arith.ML	Sat Mar 22 08:37:43 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,221 +0,0 @@
-(*  Title:  HOL/Tools/float_arith.ML
-    Author: Steven Obua
-*)
-
-signature FLOAT_ARITH =
-sig
-  exception Destruct_floatstr of string
-  val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
-
-  exception Floating_point of string
-  val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float
-  val approx_decstr_by_bin: int -> string -> Float.float * Float.float
-
-  val mk_float: Float.float -> term
-  val dest_float: term -> Float.float
-
-  val approx_float: int -> (Float.float * Float.float -> Float.float * Float.float)
-    -> string -> term * term
-end;
-
-structure FloatArith : FLOAT_ARITH =
-struct
-
-exception Destruct_floatstr of string;
-
-fun destruct_floatstr isDigit isExp number =
-  let
-    val numlist = filter (not o Char.isSpace) (String.explode number)
-
-    fun countsigns ((#"+")::cs) = countsigns cs
-      | countsigns ((#"-")::cs) =
-      let
-        val (positive, rest) = countsigns cs
-      in
-        (not positive, rest)
-      end
-      | countsigns cs = (true, cs)
-
-    fun readdigits [] = ([], [])
-      | readdigits (q as c::cs) =
-      if (isDigit c) then
-        let
-          val (digits, rest) = readdigits cs
-        in
-          (c::digits, rest)
-        end
-      else
-        ([], q)
-
-    fun readfromexp_helper cs =
-      let
-        val (positive, rest) = countsigns cs
-        val (digits, rest') = readdigits rest
-      in
-        case rest' of
-          [] => (positive, digits)
-          | _ => raise (Destruct_floatstr number)
-      end
-
-    fun readfromexp [] = (true, [])
-      | readfromexp (c::cs) =
-      if isExp c then
-        readfromexp_helper cs
-      else
-        raise (Destruct_floatstr number)
-
-    fun readfromdot [] = ([], readfromexp [])
-      | readfromdot ((#".")::cs) =
-      let
-        val (digits, rest) = readdigits cs
-        val exp = readfromexp rest
-      in
-        (digits, exp)
-      end
-      | readfromdot cs = readfromdot ((#".")::cs)
-
-    val (positive, numlist) = countsigns numlist
-    val (digits1, numlist) = readdigits numlist
-     val (digits2, exp) = readfromdot numlist
-  in
-    (positive, String.implode digits1, String.implode digits2, fst exp, String.implode (snd exp))
-  end
-
-exception Floating_point of string;
-
-val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
-fun exp5 x = Integer.pow x 5;
-fun exp10 x = Integer.pow x 10;
-fun exp2 x = Integer.pow x 2;
-
-fun find_most_significant q r =
-  let
-    fun int2real i =
-      case (Real.fromString o string_of_int) i of
-        SOME r => r
-        | NONE => raise (Floating_point "int2real")
-    fun subtract (q, r) (q', r') =
-      if r <= r' then
-        (q - q' * exp10 (r' - r), r)
-      else
-        (q * exp10 (r - r') - q', r')
-    fun bin2dec d =
-      if 0 <= d then
-        (exp2 d, 0)
-      else
-        (exp5 (~ d), d)
-
-    val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
-    val L1 = L + 1
-
-    val (q1, r1) = subtract (q, r) (bin2dec L1) 
-  in
-    if 0 <= q1 then
-      let
-        val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
-      in
-        if 0 <= q2 then
-          raise (Floating_point "find_most_significant")
-        else
-          (L1, (q1, r1))
-      end
-    else
-      let
-        val (q0, r0) = subtract (q, r) (bin2dec L)
-      in
-        if 0 <= q0 then
-          (L, (q0, r0))
-        else
-          raise (Floating_point "find_most_significant")
-      end
-  end
-
-fun approx_dec_by_bin n (q,r) =
-  let
-    fun addseq acc d' [] = acc
-      | addseq acc d' (d::ds) = addseq (acc + exp2 (d - d')) d' ds
-
-    fun seq2bin [] = (0, 0)
-      | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
-
-    fun approx d_seq d0 precision (q,r) =
-      if q = 0 then
-        let val x = seq2bin d_seq in
-          (x, x)
-        end
-      else
-        let
-          val (d, (q', r')) = find_most_significant q r
-        in
-          if precision < d0 - d then
-            let
-              val d' = d0 - precision
-              val x1 = seq2bin (d_seq)
-              val x2 = (fst x1 * exp2 (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
-            in
-              (x1, x2)
-            end
-          else
-            approx (d::d_seq) d0 precision (q', r')
-        end
-
-    fun approx_start precision (q, r) =
-      if q = 0 then
-        ((0, 0), (0, 0))
-      else
-        let
-          val (d, (q', r')) = find_most_significant q r
-        in
-          if precision <= 0 then
-            let
-              val x1 = seq2bin [d]
-            in
-              if q' = 0 then
-                (x1, x1)
-              else
-                (x1, seq2bin [d + 1])
-            end
-          else
-            approx [d] d precision (q', r')
-        end
-  in
-    if 0 <= q then
-      approx_start n (q,r)
-    else
-      let
-        val ((a1,b1), (a2, b2)) = approx_start n (~ q, r)
-      in
-        ((~ a2, b2), (~ a1, b1))
-      end
-  end
-
-fun approx_decstr_by_bin n decstr =
-  let
-    fun str2int s = the_default 0 (Int.fromString s)
-    fun signint p x = if p then x else ~ x
-
-    val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
-    val s = size d2
-
-    val q = signint p (str2int d1 * exp10 s + str2int d2)
-    val r = signint ep (str2int e) - s
-  in
-    approx_dec_by_bin n (q,r)
-  end
-
-fun mk_float (a, b) = @{term "float"} $
-  HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
-
-fun dest_float (Const ("Float.float", _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
-      pairself (snd o HOLogic.dest_number) (a, b)
-  | dest_float t = ((snd o HOLogic.dest_number) t, 0);
-
-fun approx_float prec f value =
-  let
-    val interval = approx_decstr_by_bin prec value
-    val (flower, fupper) = f interval
-  in
-    (mk_float flower, mk_float fupper)
-  end;
-
-end;
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/hologic.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -1000,7 +1000,9 @@
     cnames_syn pnames spec monos lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
+    val _ =
+      Theory.requires thy (Context.theory_name @{theory})
+        (coind_prefix coind ^ "inductive definitions");
 
 
     (* abbrevs *)
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 22 22:00:26 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 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/recdef.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -180,7 +180,7 @@
 
 (** add_recdef(_i) **)
 
-fun requires_recdef thy = Theory.requires thy "Old_Recdef" "recursive functions";
+fun requires_recdef thy = Theory.requires thy (Context.theory_name @{theory}) "recursive functions";
 
 fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
   let
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 22 22:00:26 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);
@@ -2245,7 +2245,7 @@
 
 fun add_record (params, binding) raw_parent raw_fields thy =
   let
-    val _ = Theory.requires thy "Record" "record definitions";
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "record definitions";
 
     val ctxt = Proof_Context.init_global thy;
     fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/transfer.ML	Sat Mar 22 22:00:26 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
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sat Mar 22 22:00:26 2014 +0100
@@ -1239,8 +1239,8 @@
 
   fun decomp (@{const Trueprop} $ t) =
     let fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
-        let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
-              | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
+        let fun decr (Const (@{const_name rtrancl}, _ ) $ r) = (r,"r*")
+              | decr (Const (@{const_name trancl}, _ ) $ r)  = (r,"r+")
               | decr r = (r,"r");
             val (rel,r) = decr (Envir.beta_eta_contract rel);
         in SOME (a,b,rel,r) end
@@ -1262,8 +1262,8 @@
 
   fun decomp (@{const Trueprop} $ t) =
     let fun dec (rel $ a $ b) =
-        let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $ r) = (r,"r*")
-              | decr (Const ("Transitive_Closure.tranclp", _ ) $ r)  = (r,"r+")
+        let fun decr (Const (@{const_name rtranclp}, _ ) $ r) = (r,"r*")
+              | decr (Const (@{const_name tranclp}, _ ) $ r)  = (r,"r+")
               | decr r = (r,"r");
             val (rel,r) = decr rel;
         in SOME (a, b, rel, r) end
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy	Sat Mar 22 22:00:26 2014 +0100
@@ -11,12 +11,12 @@
 imports Main
 begin
 
-ML_file "svc_funcs.ML"
-
 consts
   iff_keep :: "[bool, bool] => bool"
   iff_unfold :: "[bool, bool] => bool"
 
+ML_file "svc_funcs.ML"
+
 hide_const iff_keep iff_unfold
 
 oracle svc_oracle = Svc.oracle
diff -r 67dc9549fa15 -r fec233e7f67d src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/ex/svc_funcs.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -199,10 +199,10 @@
             Buildin("NOT", [fm (not pos) p])
       | fm pos (Const(@{const_name True}, _)) = TrueExpr
       | fm pos (Const(@{const_name False}, _)) = FalseExpr
-      | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
+      | fm pos (Const(@{const_name iff_keep}, _) $ p $ q) =
              (*polarity doesn't matter*)
             Buildin("=", [fm pos p, fm pos q])
-      | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =
+      | fm pos (Const(@{const_name iff_unfold}, _) $ p $ q) =
             Buildin("AND",   (*unfolding uses both polarities*)
                          [Buildin("=>", [fm (not pos) p, fm pos q]),
                           Buildin("=>", [fm (not pos) q, fm pos p])])
diff -r 67dc9549fa15 -r fec233e7f67d src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -121,9 +121,9 @@
       else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
 
   ML_Antiquotation.inline @{binding const}
-    (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
+    (Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) -- Scan.optional
         (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
-      >> (fn ((ctxt, raw_c), Ts) =>
+      >> (fn ((ctxt, (raw_c, pos)), Ts) =>
         let
           val Const (c, _) =
             Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
@@ -131,7 +131,7 @@
           val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
           val _ = length Ts <> n andalso
             error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
-              quote c ^ enclose "(" ")" (commas (replicate n "_")));
+              quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos);
           val const = Const (c, Consts.instance consts (c, Ts));
         in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
 
diff -r 67dc9549fa15 -r fec233e7f67d src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/ZF/OrdQuant.thy	Sat Mar 22 22:00:26 2014 +0100
@@ -357,9 +357,8 @@
 ML
 {*
 val Ord_atomize =
-    atomize ([("OrdQuant.oall", [@{thm ospec}]),("OrdQuant.rall", [@{thm rspec}])]@
-                 ZF_conn_pairs,
-             ZF_mem_pairs);
+  atomize ([(@{const_name oall}, @{thms ospec}), (@{const_name rall}, @{thms rspec})] @
+    ZF_conn_pairs, ZF_mem_pairs);
 *}
 declaration {* fn _ =>
   Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
diff -r 67dc9549fa15 -r fec233e7f67d src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -65,7 +65,7 @@
 fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
  let
   val dummy = (*has essential ancestors?*)
-    Theory.requires thy "Datatype_ZF" "(co)datatype definitions";
+    Theory.requires thy (Context.theory_name @{theory}) "(co)datatype definitions";
 
   val rec_hds = map head_of rec_tms;
 
diff -r 67dc9549fa15 -r fec233e7f67d src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Mar 22 08:37:43 2014 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Mar 22 22:00:26 2014 +0100
@@ -59,7 +59,7 @@
 fun add_inductive_i verbose (rec_tms, dom_sum)
   raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy =
 let
-  val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
+  val _ = Theory.requires thy (Context.theory_name @{theory}) "(co)inductive definitions";
   val ctxt = Proof_Context.init_global thy;
 
   val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;