# HG changeset patch
# User haftmann
# Date 1253257670 -7200
# Node ID e08fdd6153335baa78e7481d3684234d9d943085
# Parent  f2b7414738600d357cd0da8b7f7ecb0fc37afce1
tuned const_name antiquotations

diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Function/decompose.ML
--- a/src/HOL/Tools/Function/decompose.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Function/decompose.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -29,7 +29,7 @@
       fun prove_chain c1 c2 D =
           if is_some (Termination.get_chain D c1 c2) then D else
           let
-            val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name "Relation.rel_comp"} (c1, c2),
+            val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
                                       Const (@{const_name Set.empty}, fastype_of c1))
                        |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
 
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Function/fundef_common.ML
--- a/src/HOL/Tools/Function/fundef_common.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_common.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -16,7 +16,7 @@
 fun PROFILE msg = if !profile then timeap_msg msg else I
 
 
-val acc_const_name = @{const_name "accp"}
+val acc_const_name = @{const_name accp}
 fun mk_acc domT R =
     Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
 
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Function/fundef_core.ML
--- a/src/HOL/Tools/Function/fundef_core.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -769,7 +769,7 @@
       val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
       val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
 
-      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
+      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
 
       (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
       val ihyp = Term.all domT $ Abs ("z", domT,
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Function/induction_scheme.ML
--- a/src/HOL/Tools/Function/induction_scheme.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -152,7 +152,7 @@
     end
 
 fun mk_wf ctxt R (IndScheme {T, ...}) =
-    HOLogic.Trueprop $ (Const (@{const_name "wf"}, mk_relT T --> HOLogic.boolT) $ R)
+    HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
 
 fun mk_ineqs R (IndScheme {T, cases, branches}) =
     let
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -26,7 +26,7 @@
         val mlexT = (domT --> HOLogic.natT) --> relT --> relT
         fun mk_ms [] = Const (@{const_name Set.empty}, relT)
           | mk_ms (f::fs) = 
-            Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
+            Const (@{const_name mlex_prod}, mlexT) $ f $ mk_ms fs
     in
         mk_ms mfuns
     end
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Function/measure_functions.ML
--- a/src/HOL/Tools/Function/measure_functions.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -22,7 +22,7 @@
   val description = "Rules that guide the heuristic generation of measure functions"
 );
 
-fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
+fun mk_is_measures t = Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
 
 fun find_measures ctxt T =
   DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) 
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Function/sum_tree.ML
--- a/src/HOL/Tools/Function/sum_tree.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Function/sum_tree.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -17,22 +17,22 @@
 
 (* Sum types *)
 fun mk_sumT LT RT = Type ("+", [LT, RT])
-fun mk_sumcase TL TR T l r = Const (@{const_name "sum.sum_case"}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
+fun mk_sumcase TL TR T l r = Const (@{const_name sum.sum_case}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
 
 val App = curry op $
 
 fun mk_inj ST n i = 
     access_top_down 
     { init = (ST, I : term -> term),
-      left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name "Inl"}, LT --> T)))),
-      right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name "Inr"}, RT --> T))))} n i 
+      left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
+      right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i 
     |> snd
 
 fun mk_proj ST n i = 
     access_top_down 
     { init = (ST, I : term -> term),
-      left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name "Datatype.Projl"}, T --> LT)) o proj)),
-      right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name "Datatype.Projr"}, T --> RT)) o proj))} n i
+      left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name Datatype.Projl}, T --> LT)) o proj)),
+      right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name Datatype.Projr}, T --> RT)) o proj))} n i
     |> snd
 
 fun mk_sumcases T fs =
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -81,7 +81,7 @@
    else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
 | Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
    if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
-| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
+| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_)) =>
    if term_of x aconv y then
    NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
 | _ => Nox)
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -52,18 +52,18 @@
 
 local
  fun isnum t = case t of 
-   Const(@{const_name "HOL.zero"},_) => true
- | Const(@{const_name "HOL.one"},_) => true
+   Const(@{const_name HOL.zero},_) => true
+ | Const(@{const_name HOL.one},_) => true
  | @{term "Suc"}$s => isnum s
  | @{term "nat"}$s => isnum s
  | @{term "int"}$s => isnum s
- | Const(@{const_name "HOL.uminus"},_)$s => isnum s
- | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "Power.power"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name HOL.uminus},_)$s => isnum s
+ | Const(@{const_name HOL.plus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name HOL.times},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name HOL.minus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
  | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
 
  fun ty cts t = 
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -29,8 +29,8 @@
             @{const_name "op -->"}, @{const_name "op ="}] s
        then binop_conv (conv env) p 
        else atcv env p
-  | Const(@{const_name "Not"},_)$_ => arg_conv (conv env) p
-  | Const(@{const_name "Ex"},_)$Abs(s,_,_) =>
+  | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
+  | Const(@{const_name Ex},_)$Abs(s,_,_) =>
     let
      val (e,p0) = Thm.dest_comb p
      val (x,p') = Thm.dest_abs (SOME s) p0
@@ -41,8 +41,8 @@
      val (l,r) = Thm.dest_equals (cprop_of th')
     in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
        else Thm.transitive (Thm.transitive th th') (conv env r) end
-  | Const(@{const_name "Ex"},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
-  | Const(@{const_name "All"},_)$_ =>
+  | Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
+  | Const(@{const_name All},_)$_ =>
     let
      val p = Thm.dest_arg p
      val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -456,7 +456,7 @@
 fun is_cong thm =
   case (Thm.prop_of thm)
      of (Const("==>",_)$(Const("Trueprop",_)$ _) $
-         (Const("==",_) $ (Const (@{const_name "Recdef.cut"},_) $ f $ R $ a $ x) $ _)) => false
+         (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
       | _ => true;
 
 
@@ -659,7 +659,7 @@
   end;
 
 fun restricted t = isSome (S.find_term
-                            (fn (Const(@{const_name "Recdef.cut"},_)) =>true | _ => false)
+                            (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
                             t)
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -398,7 +398,7 @@
         end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
    else raise USYN_ERR "dest_relation" "not a boolean term";
 
-fun is_WFR (Const(@{const_name "Wellfounded.wf"},_)$_) = true
+fun is_WFR (Const(@{const_name Wellfounded.wf},_)$_) = true
   | is_WFR _                 = false;
 
 fun ARB ty = mk_select{Bvar=Free("v",ty),
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/float_syntax.ML
--- a/src/HOL/Tools/float_syntax.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/float_syntax.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -27,10 +27,10 @@
 fun mk_frac str =
   let
     val {mant=i, exp = n} = Syntax.read_float str;
-    val exp = Syntax.const @{const_name "Power.power"};
+    val exp = Syntax.const @{const_name Power.power};
     val ten = mk_number 10;
     val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
-  in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
+  in (Syntax.const @{const_name divide}) $ (mk_number i) $ exp10 end
 in
 
 fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -74,8 +74,8 @@
         in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
           (p (fold (Logic.all o Var) vs t) f)
         end;
-      fun mkop "op &" T x = SOME (Const (@{const_name inter}, T --> T --> T), x)
-        | mkop "op |" T x = SOME (Const (@{const_name union}, T --> T --> T), x)
+      fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
+        | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
         | mkop _ _ _ = NONE;
       fun mk_collect p T t =
         let val U = HOLogic.dest_setT T
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/int_arith.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -49,13 +49,13 @@
   make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   proc = proc1, identifier = []};
 
-fun check (Const (@{const_name "HOL.one"}, @{typ int})) = false
-  | check (Const (@{const_name "HOL.one"}, _)) = true
+fun check (Const (@{const_name HOL.one}, @{typ int})) = false
+  | check (Const (@{const_name HOL.one}, _)) = true
   | check (Const (s, _)) = member (op =) [@{const_name "op ="},
-      @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
-      @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
-      @{const_name "HOL.zero"},
-      @{const_name "HOL.less"}, @{const_name "HOL.less_eq"}] s
+      @{const_name HOL.times}, @{const_name HOL.uminus},
+      @{const_name HOL.minus}, @{const_name HOL.plus},
+      @{const_name HOL.zero},
+      @{const_name HOL.less}, @{const_name HOL.less_eq}] s
   | check (a $ b) = check a andalso check b
   | check _ = false;
 
diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -51,7 +51,7 @@
     atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
   | _ => [thm];
 
-fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name "Not"}, _) $ t)) = TP $ t
+fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
   | neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
   | neg_prop t = raise TERM ("neg_prop", [t]);