# HG changeset patch
# User wenzelm
# Date 1322834065 -3600
# Node ID 132a3e1c0fe50ef3bc991c5919e5142dfd980309
# Parent  b545ea8bc731843bd470e430ad3c79858feadfd1
more antiquotations;

diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Dec 02 14:54:25 2011 +0100
@@ -1943,8 +1943,8 @@
       term_of_num vs (@{code C} i) $ term_of_num vs t2
   | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
 
-fun term_of_fm ps vs @{code T} = HOLogic.true_const 
-  | term_of_fm ps vs @{code F} = HOLogic.false_const
+fun term_of_fm ps vs @{code T} = @{term True} 
+  | term_of_fm ps vs @{code F} = @{term False}
   | term_of_fm ps vs (@{code Lt} t) =
       @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
   | term_of_fm ps vs (@{code Le} t) =
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Dec 02 14:54:25 2011 +0100
@@ -1976,8 +1976,8 @@
       term_of_num vs (@{code C} i) $ term_of_num vs t2
   | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
 
-fun term_of_fm vs @{code T} = HOLogic.true_const 
-  | term_of_fm vs @{code F} = HOLogic.false_const
+fun term_of_fm vs @{code T} = @{term True} 
+  | term_of_fm vs @{code F} = @{term False}
   | term_of_fm vs (@{code Lt} t) = @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $
       term_of_num vs t $ @{term "0::real"}
   | term_of_fm vs (@{code Le} t) = @{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Fri Dec 02 14:54:25 2011 +0100
@@ -5602,8 +5602,8 @@
   | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
   | term_of_num vs (@{code CF} (c, t, s)) = term_of_num vs (@{code Add} (@{code Mul} (c, @{code Floor} t), s));
 
-fun term_of_fm vs @{code T} = HOLogic.true_const 
-  | term_of_fm vs @{code F} = HOLogic.false_const
+fun term_of_fm vs @{code T} = @{term True} 
+  | term_of_fm vs @{code F} = @{term False}
   | term_of_fm vs (@{code Lt} t) =
       @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::real"}
   | term_of_fm vs (@{code Le} t) =
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -1025,7 +1025,7 @@
            Goal.prove_global thy8 [] [] (augment_sort thy8 pt_cp_sort
              (HOLogic.mk_Trueprop (HOLogic.mk_eq
                (fresh c,
-                if null dts then HOLogic.true_const
+                if null dts then @{term True}
                 else foldr1 HOLogic.mk_conj (map fresh args2)))))
              (fn _ =>
                simp_tac (HOL_ss addsimps [Un_iff, empty_iff, fresh_def, supp_thm]) 1))
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -308,7 +308,7 @@
       curry (List.take o swap) (length fvars) |> map cert;
     val invs' = (case invs of
         NONE => map (fn (i, _) =>
-          Abs ("x", fastype_of (snd (nth defs' i)), HOLogic.true_const)) descr
+          Abs ("x", fastype_of (snd (nth defs' i)), @{term True})) descr
       | SOME invs' => map (prep_term lthy') invs');
     val inst = (map cert fvars ~~ cfs) @
       (map (cert o Var) pvars ~~ map cert invs') @
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -1003,8 +1003,8 @@
 
     val (((defs', vars''), ivars), (ids, thy')) =
       ((Symtab.empty |>
-        Symtab.update ("false", (HOLogic.false_const, booleanN)) |>
-        Symtab.update ("true", (HOLogic.true_const, booleanN)),
+        Symtab.update ("false", (@{term False}, booleanN)) |>
+        Symtab.update ("true", (@{term True}, booleanN)),
         Name.context),
        thy |> Sign.add_path (Long_Name.base_name ident)) |>
       fold (add_type_def prfx) (items types) |>
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -29,6 +29,7 @@
 datatype direction = Left | Right;
 
 fun treeT T = Type (@{type_name tree}, [T]);
+
 fun mk_tree' e T n [] = Const (@{const_name Tip}, treeT T)
   | mk_tree' e T n xs =
      let
@@ -38,7 +39,7 @@
        val r = mk_tree' e T (n-(m+1)) xsr;
      in
        Const (@{const_name Node}, treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $
-         l $ e x $ HOLogic.false_const $ r
+         l $ e x $ @{term False} $ r
      end
 
 fun mk_tree e T xs = mk_tree' e T (length xs) xs;
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -309,7 +309,7 @@
               val (eq, eT, nT, swap) = mkeq (dest_sel_eq t) 0;
               val prop =
                 list_all ([("n", nT), ("x", eT)],
-                  Logic.mk_equals (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
+                  Logic.mk_equals (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
               val thm = Drule.export_without_context (prove prop);
               val thm' = if swap then swap_ex_eq OF [thm] else thm
             in SOME thm' end handle TERM _ => NONE)
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -586,7 +586,7 @@
 
 (* No "real" literals means only type information (tfree_tcs, clsrel, or
    clsarity). *)
-val is_only_type_information = curry (op aconv) HOLogic.true_const
+val is_only_type_information = curry (op aconv) @{term True}
 
 fun replace_one_dependency (old, new) dep =
   if is_same_atp_step dep old then new else [dep]
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -478,7 +478,7 @@
       let val isoT = T --> Univ_elT in
         HOLogic.imp $
           (Const (set_name, UnivT') $ Datatype_Aux.mk_Free "x" Univ_elT i) $
-            (if i < length newTs then HOLogic.true_const
+            (if i < length newTs then @{term True}
              else HOLogic.mk_mem (Datatype_Aux.mk_Free "x" Univ_elT i,
                Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
                  Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T)))
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -68,8 +68,8 @@
       Datatype_Data.the_info thy tyco;
     val ty = Type (tyco, map TFree vs);
     fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT) $ t1 $ t2;
-    fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
-    fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
+    fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term True});
+    fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term False});
     val triv_injects =
       map_filter
         (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -79,7 +79,7 @@
       (case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of
          Solved thm2 => LessEq (thm2, thm)
        | Stuck thm2 =>
-         if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
+         if prems_of thm2 = [HOLogic.Trueprop $ @{term False}] then False thm2
          else None (thm2, thm)
        | _ => raise Match) (* FIXME *)
     | _ => raise Match
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Function/size.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -160,7 +160,7 @@
     fun prove_unfolded_size_eqs size_ofp fs =
       if null recTs2 then []
       else Datatype_Aux.split_conj_thm (Skip_Proof.prove ctxt xs []
-        (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l HOLogic.true_const @
+        (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l @{term True} @
            map (mk_unfolded_size_eq (AList.lookup op =
                (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
              (xs ~~ recTs2 ~~ rec_combs2))))
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -182,7 +182,7 @@
        (case try @{const_name Orderings.less_eq} of
           Solved thm2 => LessEq (thm2, thm)
         | Stuck thm2 =>
-          if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
+          if prems_of thm2 = [HOLogic.Trueprop $ @{term False}]
           then False thm2 else None (thm2, thm)
         | _ => raise Match) (* FIXME *)
      | _ => raise Match
@@ -260,7 +260,7 @@
     val pT = HOLogic.mk_prodT (T, T)
     val n = length qs
     val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
-    val conds' = if null conds then [HOLogic.true_const] else conds
+    val conds' = if null conds then [@{term True}] else conds
   in
     HOLogic.Collect_const pT $
     Abs ("uu_", pT,
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -231,7 +231,7 @@
   let val (poslits,neglits) = signed_lits th
   in  exists taut_poslit poslits
       orelse
-      exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
+      exists (member (op aconv) neglits) (@{term False} :: poslits)
   end
   handle TERM _ => false;       (*probably dest_Trueprop on a weird theorem*)
 
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -35,8 +35,8 @@
 
 (**** Transformation of Elimination Rules into First-Order Formulas****)
 
-val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
-val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
+val cfalse = cterm_of @{theory HOL} @{term False};
+val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop @{term False});
 
 (* Converts an elim-rule into an equivalent theorem that does not have the
    predicate variable. Leaves other theorems unchanged. We simply instantiate
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -653,8 +653,8 @@
   | term_of_num vs (Proc.Cn (n, i, t')) =
       term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
 
-fun term_of_fm ps vs Proc.T = HOLogic.true_const
-  | term_of_fm ps vs Proc.F = HOLogic.false_const
+fun term_of_fm ps vs Proc.T = @{term True}
+  | term_of_fm ps vs Proc.F = @{term False}
   | term_of_fm ps vs (Proc.And (t1, t2)) = HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   | term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   | term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/cnf_funcs.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -294,18 +294,18 @@
         val thm1 = simp_True_False_thm thy x
         val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
       in
-        if x' = HOLogic.false_const then
+        if x' = @{term False} then
           simp_TF_conj_False_l OF [thm1]  (* (x & y) = False *)
         else
           let
             val thm2 = simp_True_False_thm thy y
             val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
           in
-            if x' = HOLogic.true_const then
+            if x' = @{term True} then
               simp_TF_conj_True_l OF [thm1, thm2]  (* (x & y) = y' *)
-            else if y' = HOLogic.false_const then
+            else if y' = @{term False} then
               simp_TF_conj_False_r OF [thm2]  (* (x & y) = False *)
-            else if y' = HOLogic.true_const then
+            else if y' = @{term True} then
               simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
             else
               conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
@@ -316,18 +316,18 @@
         val thm1 = simp_True_False_thm thy x
         val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
       in
-        if x' = HOLogic.true_const then
+        if x' = @{term True} then
           simp_TF_disj_True_l OF [thm1]  (* (x | y) = True *)
         else
           let
             val thm2 = simp_True_False_thm thy y
             val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
           in
-            if x' = HOLogic.false_const then
+            if x' = @{term False} then
               simp_TF_disj_False_l OF [thm1, thm2]  (* (x | y) = y' *)
-            else if y' = HOLogic.true_const then
+            else if y' = @{term True} then
               simp_TF_disj_True_r OF [thm2]  (* (x | y) = True *)
-            else if y' = HOLogic.false_const then
+            else if y' = @{term False} then
               simp_TF_disj_False_r OF [thm1, thm2]  (* (x | y) = x' *)
             else
               disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/hologic.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -15,8 +15,6 @@
   val Trueprop: term
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
-  val true_const: term
-  val false_const: term
   val mk_induct_forall: typ -> term
   val mk_setT: typ -> typ
   val dest_setT: typ -> typ
@@ -162,9 +160,6 @@
 val boolN = "HOL.bool";
 val boolT = Type (boolN, []);
 
-val true_const =  Const ("HOL.True", boolT);
-val false_const = Const ("HOL.False", boolT);
-
 fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT);
 
 fun mk_setT T = T --> boolT;
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -128,7 +128,7 @@
       (if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2);
 
 fun make_bool_args' xs =
-  make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
+  make_bool_args (K @{term False}) (K @{term True}) xs;
 
 fun arg_types_of k c = drop k (binder_types (fastype_of c));
 
@@ -786,14 +786,14 @@
       in
         fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
           (Logic.strip_params r)
-          (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
+          (if null ps then @{term True} else foldr1 HOLogic.mk_conj ps)
       end;
 
     (* make a disjunction of all introduction rules *)
 
     val fp_fun =
       fold_rev lambda (p :: bs @ xs)
-        (if null intr_ts then HOLogic.false_const
+        (if null intr_ts then @{term False}
          else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
 
     (* add definiton of recursive predicates to theory *)
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -56,7 +56,7 @@
 
 fun is_False thm =
   let val _ $ t = Thm.prop_of thm
-  in t = HOLogic.false_const end;
+  in t = @{term False} end;
 
 fun is_nat t = (fastype_of1 t = HOLogic.natT);
 
@@ -349,7 +349,7 @@
   (* where ti' = HOLogic.dest_Trueprop ti                                    *)
   fun REPEAT_DETERM_etac_rev_mp tms =
     fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms)
-      HOLogic.false_const
+      @{term False}
   val split_thms  = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
   val cmap        = Splitter.cmap_of_split_thms split_thms
   val goal_tm     = REPEAT_DETERM_etac_rev_mp terms
@@ -380,7 +380,7 @@
         val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
-        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
         val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
         val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false]
       in
@@ -395,7 +395,7 @@
         val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
-        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
         val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
         val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false]
       in
@@ -413,7 +413,7 @@
                             split_type --> split_type --> HOLogic.boolT) $ zero $ t1
         val t1_lt_zero  = Const (@{const_name Orderings.less},
                             split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
-        val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
         val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
         val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
       in
@@ -437,7 +437,7 @@
         val t1_eq_t2_plus_d = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
                                 (Const (@{const_name Groups.plus},
                                   split_type --> split_type --> split_type) $ t2' $ d)
-        val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
         val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
         val subgoal2        = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
       in
@@ -458,7 +458,7 @@
                             (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
         val t1_lt_zero  = Const (@{const_name Orderings.less},
                             HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
-        val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
         val subgoal1    = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
         val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
       in
@@ -488,7 +488,7 @@
                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name Groups.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
-        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
         val subgoal2                = (map HOLogic.mk_Trueprop
                                         [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
@@ -520,7 +520,7 @@
                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name Groups.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
-        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
         val subgoal2                = (map HOLogic.mk_Trueprop
                                         [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
@@ -566,7 +566,7 @@
                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name Groups.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
-        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
         val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
                                         @ hd terms2_3
@@ -620,7 +620,7 @@
                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name Groups.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
-        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
         val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
                                         @ hd terms2_3
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/prop_logic.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -394,8 +394,8 @@
 (*       Boolean variables in the formula, similar to 'prop_formula_of_term' *)
 (*       (but the other way round).                                          *)
 
-fun term_of_prop_formula True = HOLogic.true_const
-  | term_of_prop_formula False = HOLogic.false_const
+fun term_of_prop_formula True = @{term True}
+  | term_of_prop_formula False = @{term False}
   | term_of_prop_formula (BoolVar i) = Free ("v" ^ string_of_int i, HOLogic.boolT)
   | term_of_prop_formula (Not fm) = HOLogic.mk_not (term_of_prop_formula fm)
   | term_of_prop_formula (Or (fm1, fm2)) =
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/record.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -1392,7 +1392,7 @@
              val prop =
                list_all ([("r", T)],
                  Logic.mk_equals
-                  (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
+                  (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
             in SOME (prove prop) end
             handle TERM _ => NONE)
         | _ => NONE)
@@ -1644,10 +1644,10 @@
     val inject_prop =  (* FIXME local x x' *)
       let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
         HOLogic.mk_conj (HOLogic.eq_const extT $
-          mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
+          mk_ext vars_more $ mk_ext vars_more', @{term True})
         ===
         foldr1 HOLogic.mk_conj
-          (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const])
+          (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [@{term True}])
       end;
 
     val induct_prop =
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/refute.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -2985,8 +2985,8 @@
     | Type ("prop", []) =>
         (case index_from_interpretation intr of
           ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
-        | 0  => SOME (HOLogic.mk_Trueprop HOLogic.true_const)
-        | 1  => SOME (HOLogic.mk_Trueprop HOLogic.false_const)
+        | 0  => SOME (HOLogic.mk_Trueprop @{term True})
+        | 1  => SOME (HOLogic.mk_Trueprop @{term False})
         | _  => raise REFUTE ("stlc_interpreter",
           "illegal interpretation for a propositional value"))
     | Type _  =>
diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/sat_funcs.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -288,7 +288,7 @@
   let
     (* remove premises that equal "True" *)
     val clauses' = filter (fn clause =>
-      (not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause
+      (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
         handle TERM ("dest_Trueprop", _) => true) clauses
     (* remove non-clausal premises -- of course this shouldn't actually   *)
     (* remove anything as long as 'rawsat_tac' is only called after the   *)
@@ -331,7 +331,7 @@
           if !trace_sat then
             tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
           else ()
-        val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
+        val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ @{term False})
       in
         (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
         (* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)