# HG changeset patch
# User haftmann
# Date 1253257669 -7200
# Node ID f2b7414738600d357cd0da8b7f7ecb0fc37afce1
# Parent  47d0c967c64e91e46784452863a5263cf0c7507a
more antiquotations

diff -r 47d0c967c64e -r f2b741473860 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Fri Sep 18 09:07:48 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Fri Sep 18 09:07:49 2009 +0200
@@ -79,14 +79,14 @@
 
 
 (* concrete versions for sum types *)
-fun is_inj (Const ("Sum_Type.Inl", _) $ _) = true
-  | is_inj (Const ("Sum_Type.Inr", _) $ _) = true
+fun is_inj (Const (@{const_name Sum_Type.Inl}, _) $ _) = true
+  | is_inj (Const (@{const_name Sum_Type.Inr}, _) $ _) = true
   | is_inj _ = false
 
-fun dest_inl (Const ("Sum_Type.Inl", _) $ t) = SOME t
+fun dest_inl (Const (@{const_name Sum_Type.Inl}, _) $ t) = SOME t
   | dest_inl _ = NONE
 
-fun dest_inr (Const ("Sum_Type.Inr", _) $ t) = SOME t
+fun dest_inr (Const (@{const_name Sum_Type.Inr}, _) $ t) = SOME t
   | dest_inr _ = NONE
 
 
@@ -145,8 +145,8 @@
 
 fun mk_sum_skel rel =
   let
-    val cs = FundefLib.dest_binop_list @{const_name union} rel
-    fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
+    val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
+    fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
       let
         val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
           = Term.strip_qnt_body "Ex" c
@@ -179,7 +179,7 @@
 fun get_descent (_, _, _, _, D) c m1 m2 =
   Term3tab.lookup D (c, (m1, m2))
 
-fun dest_call D (Const ("Collect", _) $ Abs (_, _, c)) =
+fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   let
     val n = get_num_points D
     val (sk, _, _, _, _) = D
@@ -233,13 +233,13 @@
 fun CALLS tac i st =
   if Thm.no_prems st then all_tac st
   else case Thm.term_of (Thm.cprem_of st i) of
-    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name union} rel, i) st
+    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
   |_ => no_tac st
 
 type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
 
 fun TERMINATION ctxt tac =
-  SUBGOAL (fn (_ $ (Const (@{const_name "wf"}, wfT) $ rel), i) =>
+  SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) =>
   let
     val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
   in
@@ -293,7 +293,7 @@
           if null ineqs then
               Const (@{const_name Set.empty}, fastype_of rel)
           else
-              foldr1 (HOLogic.mk_binop @{const_name union}) (map mk_compr ineqs)
+              foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
 
       fun solve_membership_tac i =
           (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
diff -r 47d0c967c64e -r f2b741473860 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Sep 18 09:07:48 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Sep 18 09:07:49 2009 +0200
@@ -86,13 +86,13 @@
 (** theory context references **)
 
 val inductive_forall_name = "HOL.induct_forall";
-val inductive_forall_def = thm "induct_forall_def";
+val inductive_forall_def = @{thm induct_forall_def};
 val inductive_conj_name = "HOL.induct_conj";
-val inductive_conj_def = thm "induct_conj_def";
-val inductive_conj = thms "induct_conj";
-val inductive_atomize = thms "induct_atomize";
-val inductive_rulify = thms "induct_rulify";
-val inductive_rulify_fallback = thms "induct_rulify_fallback";
+val inductive_conj_def = @{thm induct_conj_def};
+val inductive_conj = @{thms induct_conj};
+val inductive_atomize = @{thms induct_atomize};
+val inductive_rulify = @{thms induct_rulify};
+val inductive_rulify_fallback = @{thms induct_rulify_fallback};
 
 val notTrueE = TrueI RSN (2, notE);
 val notFalseI = Seq.hd (atac 1 notI);
@@ -176,7 +176,7 @@
     case concl of
       Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
     | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
-    | _ $ (Const ("HOL.ord_class.less_eq", _) $ _ $ _) =>
+    | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
       [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
          (resolve_tac [le_funI, le_boolI'])) thm))]
     | _ => [thm]