--- 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 = {}" *)
--- 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
--- 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,
--- 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
--- 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
--- 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)
--- 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 =
--- 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)
--- 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 =
--- 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)
--- 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 =
--- 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),
--- 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
--- 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
--- 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;
--- 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]);