# HG changeset patch
# User wenzelm
# Date 1395520819 -3600
# Node ID 589fafcc7cb63399d81c13036e6068f502d38f64
# Parent  1e01c159e7d91ebba19a071ca44e0137396fda5d
more antiquotations;

diff -r 1e01c159e7d9 -r 589fafcc7cb6 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Sat Mar 22 20:42:16 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Sat Mar 22 21:40:19 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 1e01c159e7d9 -r 589fafcc7cb6 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sat Mar 22 20:42:16 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sat Mar 22 21:40:19 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 1e01c159e7d9 -r 589fafcc7cb6 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sat Mar 22 20:42:16 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sat Mar 22 21:40:19 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 1e01c159e7d9 -r 589fafcc7cb6 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sat Mar 22 20:42:16 2014 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sat Mar 22 21:40:19 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