--- a/src/HOL/Decision_Procs/Approximation.thy Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Aug 19 11:02:14 2010 +0200
@@ -3301,11 +3301,11 @@
ML {*
fun reorder_bounds_tac prems i =
let
- fun variable_of_bound (Const ("Trueprop", _) $
+ fun variable_of_bound (Const (@{const_name "Trueprop"}, _) $
(Const (@{const_name Set.member}, _) $
Free (name, _) $ _)) = name
- | variable_of_bound (Const ("Trueprop", _) $
- (Const ("op =", _) $
+ | variable_of_bound (Const (@{const_name "Trueprop"}, _) $
+ (Const (@{const_name "op ="}, _) $
Free (name, _) $ _)) = name
| variable_of_bound t = raise TERM ("variable_of_bound", [t])
--- a/src/HOL/Decision_Procs/Cooper.thy Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Thu Aug 19 11:02:14 2010 +0200
@@ -1960,12 +1960,12 @@
@{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term ps vs t')
- | fm_of_term ps vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
+ | fm_of_term ps vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
let
val (xn', p') = variant_abs (xn, xT, p);
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
in @{code E} (fm_of_term ps vs' p) end
- | fm_of_term ps vs (Const ("All", _) $ Abs (xn, xT, p)) =
+ | fm_of_term ps vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
let
val (xn', p') = variant_abs (xn, xT, p);
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Aug 19 11:02:14 2010 +0200
@@ -519,9 +519,9 @@
val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
fun h x t =
case term_of t of
- Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
+ Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
else Ferrante_Rackoff_Data.Nox
- | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
+ | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
| b$y$z => if Term.could_unify (b, lt) then
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
@@ -771,7 +771,7 @@
in rth end
| _ => Thm.reflexive ct)
-| Const("op =",_)$_$Const(@{const_name Groups.zero},_) =>
+| Const(@{const_name "op ="},_)$_$Const(@{const_name Groups.zero},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -835,7 +835,7 @@
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| Const("op =",_)$a$b =>
+| Const(@{const_name "op ="},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = ctyp_of_term ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
@@ -844,7 +844,7 @@
(Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
+| @{term "Not"} $(Const(@{const_name "op ="},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
| _ => Thm.reflexive ct
end;
@@ -852,9 +852,9 @@
let
fun h x t =
case term_of t of
- Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
+ Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
else Ferrante_Rackoff_Data.Nox
- | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
+ | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
| Const(@{const_name Orderings.less},_)$y$z =>
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
--- a/src/HOL/Decision_Procs/Ferrack.thy Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Aug 19 11:02:14 2010 +0200
@@ -2000,9 +2000,9 @@
| fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
- | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
@{code E} (fm_of_term (("", dummyT) :: vs) p)
- | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
@{code A} (fm_of_term (("", dummyT) :: vs) p)
| fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
--- a/src/HOL/Decision_Procs/MIR.thy Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Aug 19 11:02:14 2010 +0200
@@ -5845,9 +5845,9 @@
@{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term vs t')
- | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
@{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
- | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
@{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
| fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Aug 19 11:02:14 2010 +0200
@@ -2960,7 +2960,7 @@
val ifft = @{term "op = :: bool => _"}
fun llt rT = Const(@{const_name Orderings.less},rrT rT);
fun lle rT = Const(@{const_name Orderings.less},rrT rT);
-fun eqt rT = Const("op =",rrT rT);
+fun eqt rT = Const(@{const_name "op ="},rrT rT);
fun rz rT = Const(@{const_name Groups.zero},rT);
fun dest_nat t = case t of
@@ -3015,26 +3015,26 @@
fun fm_of_term m m' fm =
case fm of
- Const("True",_) => @{code T}
- | Const("False",_) => @{code F}
- | Const("Not",_)$p => @{code NOT} (fm_of_term m m' p)
- | Const("op &",_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
- | Const("op |",_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
- | Const("op -->",_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
- | Const("op =",ty)$p$q =>
+ Const(@{const_name "True"},_) => @{code T}
+ | Const(@{const_name "False"},_) => @{code F}
+ | Const(@{const_name "Not"},_)$p => @{code NOT} (fm_of_term m m' p)
+ | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name "op ="},ty)$p$q =>
if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
| Const(@{const_name Orderings.less},_)$p$q =>
@{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
| Const(@{const_name Orderings.less_eq},_)$p$q =>
@{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
- | Const("Ex",_)$Abs(xn,xT,p) =>
+ | Const(@{const_name "Ex"},_)$Abs(xn,xT,p) =>
let val (xn', p') = variant_abs (xn,xT,p)
val x = Free(xn',xT)
fun incr i = i + 1
val m0 = (x,0):: (map (apsnd incr) m)
in @{code E} (fm_of_term m0 m' p') end
- | Const("All",_)$Abs(xn,xT,p) =>
+ | Const(@{const_name "All"},_)$Abs(xn,xT,p) =>
let val (xn', p') = variant_abs (xn,xT,p)
val x = Free(xn',xT)
fun incr i = i + 1
@@ -3045,8 +3045,8 @@
fun term_of_fm T m m' t =
case t of
- @{code T} => Const("True",bT)
- | @{code F} => Const("False",bT)
+ @{code T} => Const(@{const_name "True"},bT)
+ | @{code F} => Const(@{const_name "False"},bT)
| @{code NOT} p => nott $ (term_of_fm T m m' p)
| @{code And} (p,q) => conjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
| @{code Or} (p,q) => disjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
--- a/src/HOL/Decision_Procs/cooper_tac.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Thu Aug 19 11:02:14 2010 +0200
@@ -110,7 +110,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
- Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
+ Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
in
((pth RS iffD2) RS pre_thm,
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Thu Aug 19 11:02:14 2010 +0200
@@ -91,7 +91,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case prop_of pre_thm of
- Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
+ Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
in
(trace_msg ("calling procedure with term:\n" ^
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Aug 19 11:02:14 2010 +0200
@@ -33,12 +33,12 @@
{isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
let
fun uset (vars as (x::vs)) p = case term_of p of
- Const("op &", _)$ _ $ _ =>
+ Const(@{const_name "op &"}, _)$ _ $ _ =>
let
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
val (lS,lth) = uset vars l val (rS, rth) = uset vars r
in (lS@rS, Drule.binop_cong_rule b lth rth) end
- | Const("op |", _)$ _ $ _ =>
+ | Const(@{const_name "op |"}, _)$ _ $ _ =>
let
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
val (lS,lth) = uset vars l val (rS, rth) = uset vars r
@@ -77,7 +77,7 @@
fun main vs p =
let
val ((xn,ce),(x,fm)) = (case term_of p of
- Const("Ex",_)$Abs(xn,xT,_) =>
+ Const(@{const_name "Ex"},_)$Abs(xn,xT,_) =>
Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
| _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
val cT = ctyp_of_term x
@@ -122,12 +122,12 @@
fun decomp_mpinf fm =
case term_of fm of
- Const("op &",_)$_$_ =>
+ Const(@{const_name "op &"},_)$_$_ =>
let val (p,q) = Thm.dest_binop fm
in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
(Thm.cabs x p) (Thm.cabs x q))
end
- | Const("op |",_)$_$_ =>
+ | Const(@{const_name "op |"},_)$_$_ =>
let val (p,q) = Thm.dest_binop fm
in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
(Thm.cabs x p) (Thm.cabs x q))
@@ -175,19 +175,19 @@
let
fun h bounds tm =
(case term_of tm of
- Const ("op =", T) $ _ $ _ =>
+ Const (@{const_name "op ="}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else Thm.dest_fun2 tm
- | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
- | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("op &", _) $ _ $ _ => find_args bounds tm
- | Const ("op |", _) $ _ $ _ => find_args bounds tm
- | Const ("op -->", _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
| Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
and find_args bounds tm =
(h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
--- a/src/HOL/Decision_Procs/langford.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Thu Aug 19 11:02:14 2010 +0200
@@ -30,7 +30,7 @@
fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
case term_of ep of
- Const("Ex",_)$_ =>
+ Const(@{const_name "Ex"},_)$_ =>
let
val p = Thm.dest_arg ep
val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid)
@@ -116,13 +116,13 @@
fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
fun is_eqx x eq = case term_of eq of
- Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x
+ Const(@{const_name "op ="},_)$l$r => l aconv term_of x orelse r aconv term_of x
| _ => false ;
local
fun proc ct =
case term_of ct of
- Const("Ex",_)$Abs (xn,_,_) =>
+ Const(@{const_name "Ex"},_)$Abs (xn,_,_) =>
let
val e = Thm.dest_fun ct
val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
@@ -176,19 +176,19 @@
let
fun h bounds tm =
(case term_of tm of
- Const ("op =", T) $ _ $ _ =>
+ Const (@{const_name "op ="}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else Thm.dest_fun2 tm
- | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
- | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("op &", _) $ _ $ _ => find_args bounds tm
- | Const ("op |", _) $ _ $ _ => find_args bounds tm
- | Const ("op -->", _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
- | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
and find_args bounds tm =
(h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
--- a/src/HOL/Decision_Procs/mir_tac.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Thu Aug 19 11:02:14 2010 +0200
@@ -132,7 +132,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
- Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
+ Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
let val pth =
(* If quick_and_dirty then run without proof generation as oracle*)
if !quick_and_dirty
--- a/src/HOL/Import/proof_kernel.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Thu Aug 19 11:02:14 2010 +0200
@@ -1007,7 +1007,7 @@
local
val th = thm "not_def"
val thy = theory_of_thm th
- val pp = Thm.reflexive (cterm_of thy (Const("Trueprop",boolT-->propT)))
+ val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},boolT-->propT)))
in
val not_elim_thm = Thm.combination pp th
end
@@ -1053,9 +1053,9 @@
val c = prop_of th3
val vname = fst(dest_Free v)
val (cold,cnew) = case c of
- tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) =>
+ tpc $ (Const(@{const_name "All"},allT) $ Abs(oldname,ty,body)) =>
(Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
- | tpc $ (Const("All",allT) $ rest) => (tpc,tpc)
+ | tpc $ (Const(@{const_name "All"},allT) $ rest) => (tpc,tpc)
| _ => raise ERR "mk_GEN" "Unknown conclusion"
val th4 = Thm.rename_boundvars cold cnew th3
val res = implies_intr_hyps th4
@@ -1476,10 +1476,10 @@
fun mk_COMB th1 th2 thy =
let
val (f,g) = case concl_of th1 of
- _ $ (Const("op =",_) $ f $ g) => (f,g)
+ _ $ (Const(@{const_name "op ="},_) $ f $ g) => (f,g)
| _ => raise ERR "mk_COMB" "First theorem not an equality"
val (x,y) = case concl_of th2 of
- _ $ (Const("op =",_) $ x $ y) => (x,y)
+ _ $ (Const(@{const_name "op ="},_) $ x $ y) => (x,y)
| _ => raise ERR "mk_COMB" "Second theorem not an equality"
val fty = type_of f
val (fd,fr) = dom_rng fty
@@ -1521,7 +1521,7 @@
val th1 = norm_hyps th1
val th2 = norm_hyps th2
val (l,r) = case concl_of th of
- _ $ (Const("op |",_) $ l $ r) => (l,r)
+ _ $ (Const(@{const_name "op |"},_) $ l $ r) => (l,r)
| _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
@@ -1654,7 +1654,7 @@
val cwit = cterm_of thy wit'
val cty = ctyp_of_term cwit
val a = case ex' of
- (Const("Ex",_) $ a) => a
+ (Const(@{const_name "Ex"},_) $ a) => a
| _ => raise ERR "EXISTS" "Argument not existential"
val ca = cterm_of thy a
val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
@@ -1687,7 +1687,7 @@
val c = HOLogic.dest_Trueprop (concl_of th2)
val cc = cterm_of thy c
val a = case concl_of th1 of
- _ $ (Const("Ex",_) $ a) => a
+ _ $ (Const(@{const_name "Ex"},_) $ a) => a
| _ => raise ERR "CHOOSE" "Conclusion not existential"
val ca = cterm_of (theory_of_thm th1) a
val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
@@ -1773,7 +1773,7 @@
val (info',tm') = disamb_term_from info tm
val th = norm_hyps th
val ct = cterm_of thy tm'
- val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th
+ val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name "Not"},boolT-->boolT) $ tm')) th
val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
val res = HOLThm(rens_of info',res1)
@@ -1788,7 +1788,7 @@
val cv = cterm_of thy v
val th1 = implies_elim_all (beta_eta_thm th)
val (f,g) = case concl_of th1 of
- _ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
+ _ $ (Const(@{const_name "op ="},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
| _ => raise ERR "mk_ABS" "Bad conclusion"
val (fd,fr) = dom_rng (type_of f)
val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
@@ -1860,7 +1860,7 @@
val _ = if_debug pth hth
val th1 = implies_elim_all (beta_eta_thm th)
val a = case concl_of th1 of
- _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
+ _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name "False"},_)) => a
| _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
val ca = cterm_of thy a
val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
@@ -1877,7 +1877,7 @@
val _ = if_debug pth hth
val th1 = implies_elim_all (beta_eta_thm th)
val a = case concl_of th1 of
- _ $ (Const("Not",_) $ a) => a
+ _ $ (Const(@{const_name "Not"},_) $ a) => a
| _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
val ca = cterm_of thy a
val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
@@ -1996,7 +1996,7 @@
("x",dT,body $ Bound 0)
end
handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
- fun dest_exists (Const("Ex",_) $ abody) =
+ fun dest_exists (Const(@{const_name "Ex"},_) $ abody) =
dest_eta_abs abody
| dest_exists tm =
raise ERR "new_specification" "Bad existential formula"
@@ -2082,7 +2082,7 @@
val (HOLThm(rens,td_th)) = norm_hthm thy hth
val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
val c = case concl_of th2 of
- _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
+ _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
| _ => raise ERR "new_type_definition" "Bad type definition theorem"
val tfrees = OldTerm.term_tfrees c
val tnames = map fst tfrees
@@ -2108,7 +2108,7 @@
val rew = rewrite_hol4_term (concl_of td_th) thy4
val th = Thm.equal_elim rew (Thm.transfer thy4 td_th)
val c = case HOLogic.dest_Trueprop (prop_of th) of
- Const("Ex",exT) $ P =>
+ Const(@{const_name "Ex"},exT) $ P =>
let
val PT = domain_type exT
in
@@ -2157,7 +2157,7 @@
SOME (cterm_of thy t)] light_nonempty
val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
val c = case concl_of th2 of
- _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
+ _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
| _ => raise ERR "type_introduction" "Bad type definition theorem"
val tfrees = OldTerm.term_tfrees c
val tnames = sort_strings (map fst tfrees)
--- a/src/HOL/Import/shuffler.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Thu Aug 19 11:02:14 2010 +0200
@@ -60,14 +60,14 @@
fun mk_meta_eq th =
(case concl_of th of
- Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
+ Const(@{const_name "Trueprop"},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
| Const("==",_) $ _ $ _ => th
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make meta equality",0,[th]) (* FIXME avoid handle _ *)
fun mk_obj_eq th =
(case concl_of th of
- Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
+ Const(@{const_name "Trueprop"},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
| Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make object equality",0,[th]) (* FIXME avoid handle _ *)
--- a/src/HOL/Library/Eval_Witness.thy Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Thu Aug 19 11:02:14 2010 +0200
@@ -63,7 +63,7 @@
else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
fun dest_exs 0 t = t
- | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) =
+ | dest_exs n (Const (@{const_name "Ex"}, _) $ Abs (v,T,b)) =
Abs (v, check_type T, dest_exs (n - 1) b)
| dest_exs _ _ = sys_error "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
--- a/src/HOL/Library/positivstellensatz.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Thu Aug 19 11:02:14 2010 +0200
@@ -498,7 +498,7 @@
val strip_exists =
let fun h (acc, t) =
case (term_of t) of
- Const("Ex",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+ Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
@@ -515,7 +515,7 @@
fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
fun choose v th th' = case concl_of th of
- @{term Trueprop} $ (Const("Ex",_)$_) =>
+ @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) =>
let
val p = (funpow 2 Thm.dest_arg o cprop_of) th
val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
@@ -533,7 +533,7 @@
val strip_forall =
let fun h (acc, t) =
case (term_of t) of
- Const("All",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+ Const(@{const_name "All"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
--- a/src/HOL/Library/reflection.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Library/reflection.ML Thu Aug 19 11:02:14 2010 +0200
@@ -82,7 +82,7 @@
fun rearrange congs =
let
fun P (_, th) =
- let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th
+ let val @{term "Trueprop"}$(Const (@{const_name "op ="},_) $l$_) = concl_of th
in can dest_Var l end
val (yes,no) = List.partition P congs
in no @ yes end
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Aug 19 11:02:14 2010 +0200
@@ -183,7 +183,7 @@
end;
fun mk_not_sym ths = maps (fn th => case prop_of th of
- _ $ (Const ("Not", _) $ (Const ("op =", _) $ _ $ _)) => [th, th RS not_sym]
+ _ $ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
| _ => [th]) ths;
fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
@@ -1372,7 +1372,7 @@
SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
_ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
simp_tac ind_ss1' i
- | _ $ (Const ("Not", _) $ _) =>
+ | _ $ (Const (@{const_name "Not"}, _) $ _) =>
resolve_tac freshs2' i
| _ => asm_simp_tac (HOL_basic_ss addsimps
pt2_atoms addsimprocs [perm_simproc]) i)) 1])
@@ -1671,7 +1671,7 @@
val rec_unique_frees' =
Datatype_Prop.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
val rec_unique_concls = map (fn ((x, U), R) =>
- Const ("Ex1", (U --> HOLogic.boolT) --> HOLogic.boolT) $
+ Const (@{const_name "Ex1"}, (U --> HOLogic.boolT) --> HOLogic.boolT) $
Abs ("y", U, R $ Free x $ Bound 0))
(rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
@@ -1777,7 +1777,7 @@
| _ => false) prems';
val fresh_prems = filter (fn th => case prop_of th of
_ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
- | _ $ (Const ("Not", _) $ _) => true
+ | _ $ (Const (@{const_name "Not"}, _) $ _) => true
| _ => false) prems';
val Ts = map fastype_of boundsl;
@@ -1879,7 +1879,7 @@
end) rec_prems2;
val ihs = filter (fn th => case prop_of th of
- _ $ (Const ("All", _) $ _) => true | _ => false) prems';
+ _ $ (Const (@{const_name "All"}, _) $ _) => true | _ => false) prems';
(** pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs **)
val _ = warning "step 7: pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs";
@@ -2022,7 +2022,7 @@
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
(Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
- Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
+ Const (@{const_name "The"}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Aug 19 11:02:14 2010 +0200
@@ -71,14 +71,14 @@
| add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
| add_binders thy i _ bs = bs;
-fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (f p q) else NONE
| _ => NONE)
| split_conj _ _ _ _ = NONE;
fun strip_all [] t = t
- | strip_all (_ :: xs) (Const ("All", _) $ Abs (s, T, t)) = strip_all xs t;
+ | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
(*********************************************************************)
(* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *)
@@ -89,7 +89,7 @@
(* where "id" protects the subformula from simplification *)
(*********************************************************************)
-fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
(case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (HOLogic.mk_conj (p,
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Aug 19 11:02:14 2010 +0200
@@ -75,14 +75,14 @@
| add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
| add_binders thy i _ bs = bs;
-fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (f p q) else NONE
| _ => NONE)
| split_conj _ _ _ _ = NONE;
fun strip_all [] t = t
- | strip_all (_ :: xs) (Const ("All", _) $ Abs (s, T, t)) = strip_all xs t;
+ | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
(*********************************************************************)
(* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *)
@@ -93,7 +93,7 @@
(* where "id" protects the subformula from simplification *)
(*********************************************************************)
-fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
(case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (HOLogic.mk_conj (p,
--- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Aug 19 11:02:14 2010 +0200
@@ -135,7 +135,7 @@
val thy = Context.theory_of context
val thms_to_be_added = (case (prop_of orig_thm) of
(* case: eqvt-lemma is of the implicational form *)
- (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
+ (Const("==>", _) $ (Const (@{const_name "Trueprop"},_) $ hyp) $ (Const (@{const_name "Trueprop"},_) $ concl)) =>
let
val (pi,typi) = get_pi concl thy
in
--- a/src/HOL/Prolog/prolog.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML Thu Aug 19 11:02:14 2010 +0200
@@ -10,17 +10,17 @@
exception not_HOHH;
fun isD t = case t of
- Const("Trueprop",_)$t => isD t
- | Const("op &" ,_)$l$r => isD l andalso isD r
- | Const("op -->",_)$l$r => isG l andalso isD r
+ Const(@{const_name "Trueprop"},_)$t => isD t
+ | Const(@{const_name "op &"} ,_)$l$r => isD l andalso isD r
+ | Const(@{const_name "op -->"},_)$l$r => isG l andalso isD r
| Const( "==>",_)$l$r => isG l andalso isD r
- | Const("All",_)$Abs(s,_,t) => isD t
+ | Const(@{const_name "All"},_)$Abs(s,_,t) => isD t
| Const("all",_)$Abs(s,_,t) => isD t
- | Const("op |",_)$_$_ => false
- | Const("Ex" ,_)$_ => false
+ | Const(@{const_name "op |"},_)$_$_ => false
+ | Const(@{const_name "Ex"} ,_)$_ => false
| Const("not",_)$_ => false
- | Const("True",_) => false
- | Const("False",_) => false
+ | Const(@{const_name "True"},_) => false
+ | Const(@{const_name "False"},_) => false
| l $ r => isD l
| Const _ (* rigid atom *) => true
| Bound _ (* rigid atom *) => true
@@ -29,17 +29,17 @@
anything else *) => false
and
isG t = case t of
- Const("Trueprop",_)$t => isG t
- | Const("op &" ,_)$l$r => isG l andalso isG r
- | Const("op |" ,_)$l$r => isG l andalso isG r
- | Const("op -->",_)$l$r => isD l andalso isG r
+ Const(@{const_name "Trueprop"},_)$t => isG t
+ | Const(@{const_name "op &"} ,_)$l$r => isG l andalso isG r
+ | Const(@{const_name "op |"} ,_)$l$r => isG l andalso isG r
+ | Const(@{const_name "op -->"},_)$l$r => isD l andalso isG r
| Const( "==>",_)$l$r => isD l andalso isG r
- | Const("All",_)$Abs(_,_,t) => isG t
+ | Const(@{const_name "All"},_)$Abs(_,_,t) => isG t
| Const("all",_)$Abs(_,_,t) => isG t
- | Const("Ex" ,_)$Abs(_,_,t) => isG t
- | Const("True",_) => true
+ | Const(@{const_name "Ex"} ,_)$Abs(_,_,t) => isG t
+ | Const(@{const_name "True"},_) => true
| Const("not",_)$_ => false
- | Const("False",_) => false
+ | Const(@{const_name "False"},_) => false
| _ (* atom *) => true;
val check_HOHH_tac1 = PRIMITIVE (fn thm =>
@@ -51,10 +51,10 @@
fun atomizeD ctxt thm = let
fun at thm = case concl_of thm of
- _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS
+ _$(Const(@{const_name "All"} ,_)$Abs(s,_,_))=> at(thm RS
(read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
- | _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
- | _$(Const("op -->",_)$_$_) => at(thm RS mp)
+ | _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ | _$(Const(@{const_name "op -->"},_)$_$_) => at(thm RS mp)
| _ => [thm]
in map zero_var_indexes (at thm) end;
@@ -71,15 +71,15 @@
resolve_tac (maps atomizeD prems) 1);
-- is nice, but cannot instantiate unknowns in the assumptions *)
fun hyp_resolve_tac i st = let
- fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
- | ap (Const("op -->",_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
+ fun ap (Const(@{const_name "All"},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
+ | ap (Const(@{const_name "op -->"},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
| ap t = (0,false,t);
(*
fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
| rep_goal (Const ("==>",_)$s$t) =
(case rep_goal t of (l,t) => (s::l,t))
| rep_goal t = ([] ,t);
- val (prems, Const("Trueprop", _)$concl) = rep_goal
+ val (prems, Const(@{const_name "Trueprop"}, _)$concl) = rep_goal
(#3(dest_state (st,i)));
*)
val subgoal = #3(Thm.dest_state (st,i));
--- a/src/HOL/Statespace/distinct_tree_prover.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Thu Aug 19 11:02:14 2010 +0200
@@ -343,7 +343,7 @@
end handle Option => NONE)
fun distinctTree_tac names ctxt
- (Const ("Trueprop",_) $ (Const ("Not", _) $ (Const ("op =", _) $ x $ y)), i) =
+ (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
(case get_fst_success (neq_x_y ctxt x y) names of
SOME neq => rtac neq i
| NONE => no_tac)
@@ -356,7 +356,7 @@
fun distinct_simproc names =
Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
- (fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
+ (fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
case try Simplifier.the_context ss of
SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq])
(get_fst_success (neq_x_y ctxt x y) names)
--- a/src/HOL/Statespace/state_fun.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Thu Aug 19 11:02:14 2010 +0200
@@ -43,9 +43,9 @@
val conj_True = thm "conj_True";
val conj_cong = thm "conj_cong";
-fun isFalse (Const ("False",_)) = true
+fun isFalse (Const (@{const_name "False"},_)) = true
| isFalse _ = false;
-fun isTrue (Const ("True",_)) = true
+fun isTrue (Const (@{const_name "True"},_)) = true
| isTrue _ = false;
in
@@ -53,7 +53,7 @@
val lazy_conj_simproc =
Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"]
(fn thy => fn ss => fn t =>
- (case t of (Const ("op &",_)$P$Q) =>
+ (case t of (Const (@{const_name "op &"},_)$P$Q) =>
let
val P_P' = Simplifier.rewrite ss (cterm_of thy P);
val P' = P_P' |> prop_of |> Logic.dest_equals |> #2
@@ -285,7 +285,7 @@
then Bound 2
else raise TERM ("",[n]);
val sel' = lo $ d $ n' $ s;
- in (Const ("op =",Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
+ in (Const (@{const_name "op ="},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
fun dest_state (s as Bound 0) = s
| dest_state (s as (Const (sel,sT)$Bound 0)) =
@@ -295,20 +295,20 @@
| dest_state s =
raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
- fun dest_sel_eq (Const ("op =",Teq)$
+ fun dest_sel_eq (Const (@{const_name "op ="},Teq)$
((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
(false,Teq,lT,lo,d,n,X,dest_state s)
- | dest_sel_eq (Const ("op =",Teq)$X$
+ | dest_sel_eq (Const (@{const_name "op ="},Teq)$X$
((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
(true,Teq,lT,lo,d,n,X,dest_state s)
| dest_sel_eq _ = raise TERM ("",[]);
in
(case t of
- (Const ("Ex",Tex)$Abs(s,T,t)) =>
+ (Const (@{const_name "Ex"},Tex)$Abs(s,T,t)) =>
(let val (eq,eT,nT,swap) = mkeq (dest_sel_eq t) 0;
val prop = list_all ([("n",nT),("x",eT)],
- Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq),
+ Logic.mk_equals (Const (@{const_name "Ex"},Tex)$Abs(s,T,eq),
HOLogic.true_const));
val thm = Drule.export_without_context (prove prop);
val thm' = if swap then swap_ex_eq OF [thm] else thm
@@ -367,7 +367,7 @@
val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
val (lookup_ss', ex_lookup_ss') =
(case (concl_of thm) of
- (_$((Const ("Ex",_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
+ (_$((Const (@{const_name "Ex"},_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
| _ => (lookup_ss addsimps [thm], ex_lookup_ss))
fun activate_simprocs ctxt =
if simprocs_active then ctxt
--- a/src/HOL/Statespace/state_space.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu Aug 19 11:02:14 2010 +0200
@@ -222,8 +222,8 @@
end handle Option => NONE)
fun distinctTree_tac ctxt
- (Const ("Trueprop",_) $
- (Const ("Not", _) $ (Const ("op =", _) $ (x as Free _)$ (y as Free _))), i) =
+ (Const (@{const_name "Trueprop"},_) $
+ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
(case (neq_x_y ctxt x y) of
SOME neq => rtac neq i
| NONE => no_tac)
@@ -236,7 +236,7 @@
val distinct_simproc =
Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
- (fn thy => fn ss => (fn (Const ("op =",_)$(x as Free _)$(y as Free _)) =>
+ (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
(case try Simplifier.the_context ss of
SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
(neq_x_y ctxt x y)
--- a/src/HOL/TLA/Intensional.thy Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/TLA/Intensional.thy Thu Aug 19 11:02:14 2010 +0200
@@ -279,7 +279,7 @@
fun hflatten t =
case (concl_of t) of
- Const _ $ (Const ("op -->", _) $ _ $ _) => hflatten (t RS mp)
+ Const _ $ (Const (@{const_name "op -->"}, _) $ _ $ _) => hflatten (t RS mp)
| _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
in
hflatten t
--- a/src/HOL/Tools/Function/function_core.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Thu Aug 19 11:02:14 2010 +0200
@@ -392,7 +392,7 @@
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
val ihyp = Term.all domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
- HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
+ HOLogic.mk_Trueprop (Const (@{const_name "Ex1"}, (ranT --> boolT) --> boolT) $
Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
|> cterm_of thy
--- a/src/HOL/Tools/Function/termination.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML Thu Aug 19 11:02:14 2010 +0200
@@ -148,7 +148,7 @@
val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
- val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
+ val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
= Term.strip_qnt_body "Ex" c
in cons r o cons l end
in
@@ -185,7 +185,7 @@
val vs = Term.strip_qnt_vars "Ex" c
(* FIXME: throw error "dest_call" for malformed terms *)
- val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
+ val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
= Term.strip_qnt_body "Ex" c
val (p, l') = dest_inj sk l
val (q, r') = dest_inj sk r
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 19 11:02:14 2010 +0200
@@ -147,7 +147,7 @@
fun Trueprop_conv cv ct =
case Thm.term_of ct of
- Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct
+ Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct
| _ => raise Fail "Trueprop_conv"
fun preprocess_intro thy rule =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Aug 19 11:02:14 2010 +0200
@@ -405,13 +405,13 @@
(* general syntactic functions *)
(*Like dest_conj, but flattens conjunctions however nested*)
-fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+fun conjuncts_aux (Const (@{const_name "op &"}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
| conjuncts_aux t conjs = t::conjs;
fun conjuncts t = conjuncts_aux t [];
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
- | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
+ | is_equationlike_term (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
| is_equationlike_term _ = false
val is_equationlike = is_equationlike_term o prop_of
@@ -482,7 +482,7 @@
fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
-fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
+fun strip_ex (Const (@{const_name "Ex"}, _) $ Abs (x, T, t)) =
let
val (xTs, t') = strip_ex t
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 19 11:02:14 2010 +0200
@@ -524,7 +524,7 @@
fun dest_conjunct_prem th =
case HOLogic.dest_Trueprop (prop_of th) of
- (Const ("op &", _) $ t $ t') =>
+ (Const (@{const_name "op &"}, _) $ t $ t') =>
dest_conjunct_prem (th RS @{thm conjunct1})
@ dest_conjunct_prem (th RS @{thm conjunct2})
| _ => [th]
@@ -576,7 +576,7 @@
fun Trueprop_conv cv ct =
case Thm.term_of ct of
- Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct
+ Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct
| _ => raise Fail "Trueprop_conv"
fun preprocess_intro thy rule =
@@ -587,7 +587,7 @@
fun preprocess_elim ctxt elimrule =
let
- fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
+ fun replace_eqs (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
| replace_eqs t = t
val thy = ProofContext.theory_of ctxt
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Aug 19 11:02:14 2010 +0200
@@ -111,7 +111,7 @@
fun mk_meta_equation th =
case prop_of th of
- Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
+ Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
| _ => th
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Aug 19 11:02:14 2010 +0200
@@ -86,11 +86,11 @@
map instantiate rew_ths
end
-fun is_compound ((Const ("Not", _)) $ t) =
+fun is_compound ((Const (@{const_name "Not"}, _)) $ t) =
error "is_compound: Negation should not occur; preprocessing is defect"
- | is_compound ((Const ("Ex", _)) $ _) = true
+ | is_compound ((Const (@{const_name "Ex"}, _)) $ _) = true
| is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
- | is_compound ((Const ("op &", _)) $ _ $ _) =
+ | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
error "is_compound: Conjunction should not occur; preprocessing is defect"
| is_compound _ = false
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Aug 19 11:02:14 2010 +0200
@@ -168,10 +168,10 @@
mk_split_lambda' xs t
end;
-fun strip_imp_prems (Const("op -->", _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
| strip_imp_prems _ = [];
-fun strip_imp_concl (Const("op -->", _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
| strip_imp_concl A = A : term;
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Aug 19 11:02:14 2010 +0200
@@ -120,10 +120,10 @@
fun whatis x ct =
( case (term_of ct) of
- Const("op &",_)$_$_ => And (Thm.dest_binop ct)
-| Const ("op |",_)$_$_ => Or (Thm.dest_binop ct)
-| Const ("op =",_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
-| Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
+ Const(@{const_name "op &"},_)$_$_ => And (Thm.dest_binop ct)
+| Const (@{const_name "op |"},_)$_$_ => Or (Thm.dest_binop ct)
+| Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
+| Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
| Const (@{const_name Orderings.less}, _) $ y$ z =>
if term_of x aconv y then Lt (Thm.dest_arg ct)
@@ -274,7 +274,7 @@
| lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
| lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
- | lin (vs as x::_) ((b as Const("op =",_))$s$t) =
+ | lin (vs as x::_) ((b as Const(@{const_name "op ="},_))$s$t) =
(case lint vs (subC$t$s) of
(t as a$(m$c$y)$r) =>
if x <> y then b$zero$t
@@ -353,8 +353,8 @@
then (ins (dest_number c) acc, dacc) else (acc,dacc)
| Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
- | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
- | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+ | Const(@{const_name "op &"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+ | Const(@{const_name "op |"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
| Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
| _ => (acc, dacc)
val (cs,ds) = h ([],[]) p
@@ -382,8 +382,8 @@
end
fun unit_conv t =
case (term_of t) of
- Const("op &",_)$_$_ => Conv.binop_conv unit_conv t
- | Const("op |",_)$_$_ => Conv.binop_conv unit_conv t
+ Const(@{const_name "op &"},_)$_$_ => Conv.binop_conv unit_conv t
+ | Const(@{const_name "op |"},_)$_$_ => Conv.binop_conv unit_conv t
| Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
| Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
@@ -612,19 +612,19 @@
fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
| fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
- | fm_of_term ps vs (Const ("op &", _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name "op &"}, _) $ t1 $ t2) =
Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (Const ("op |", _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (Const ("op -->", _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name "op -->"}, _) $ t1 $ t2) =
Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (Const (@{const_name Not}, _) $ t') =
Proc.Not (fm_of_term ps vs t')
- | fm_of_term ps vs (Const ("Ex", _) $ Abs abs) =
+ | fm_of_term ps vs (Const (@{const_name "Ex"}, _) $ Abs abs) =
Proc.E (uncurry (fm_of_term ps) (descend vs abs))
- | fm_of_term ps vs (Const ("All", _) $ Abs abs) =
+ | fm_of_term ps vs (Const (@{const_name "All"}, _) $ Abs abs) =
Proc.A (uncurry (fm_of_term ps) (descend vs abs))
| fm_of_term ps vs (@{term "op = :: int => _"} $ t1 $ t2) =
Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
@@ -687,14 +687,14 @@
fun strip_objimp ct =
(case Thm.term_of ct of
- Const ("op -->", _) $ _ $ _ =>
+ Const (@{const_name "op -->"}, _) $ _ $ _ =>
let val (A, B) = Thm.dest_binop ct
in A :: strip_objimp B end
| _ => [ct]);
fun strip_objall ct =
case term_of ct of
- Const ("All", _) $ Abs (xn,xT,p) =>
+ Const (@{const_name "All"}, _) $ Abs (xn,xT,p) =>
let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
in apfst (cons (a,v)) (strip_objall t')
end
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 19 11:02:14 2010 +0200
@@ -308,7 +308,7 @@
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
- Const ("op =", HOLogic.typeT)
+ Const (@{const_name "op ="}, HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
(case strip_prefix_and_undo_ascii const_prefix x of
SOME c => Const (invert_const c, dummyT)
--- a/src/HOL/Tools/TFL/post.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/TFL/post.ML Thu Aug 19 11:02:14 2010 +0200
@@ -67,7 +67,7 @@
val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
fun mk_meta_eq r = case concl_of r of
Const("==",_)$_$_ => r
- | _ $(Const("op =",_)$_$_) => r RS eq_reflection
+ | _ $(Const(@{const_name "op ="},_)$_$_) => r RS eq_reflection
| _ => r RS P_imp_P_eq_True
(*Is this the best way to invoke the simplifier??*)
--- a/src/HOL/Tools/TFL/rules.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Thu Aug 19 11:02:14 2010 +0200
@@ -453,14 +453,14 @@
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
fun is_cong thm =
case (Thm.prop_of thm)
- of (Const("==>",_)$(Const("Trueprop",_)$ _) $
+ of (Const("==>",_)$(Const(@{const_name "Trueprop"},_)$ _) $
(Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
| _ => true;
fun dest_equal(Const ("==",_) $
- (Const ("Trueprop",_) $ lhs)
- $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
+ (Const (@{const_name "Trueprop"},_) $ lhs)
+ $ (Const (@{const_name "Trueprop"},_) $ rhs)) = {lhs=lhs, rhs=rhs}
| dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
| dest_equal tm = S.dest_eq tm;
@@ -759,7 +759,7 @@
val cntxt = rev(Simplifier.prems_of_ss ss)
val dummy = print_thms "cntxt:" cntxt
val thy = Thm.theory_of_thm thm
- val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
+ val Const("==>",_) $ (Const(@{const_name "Trueprop"},_) $ A) $ _ = Thm.prop_of thm
fun genl tm = let val vlist = subtract (op aconv) globals
(OldTerm.add_term_frees(tm,[]))
in fold_rev Forall vlist tm
--- a/src/HOL/Tools/TFL/tfl.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Thu Aug 19 11:02:14 2010 +0200
@@ -483,7 +483,7 @@
val (case_rewrites,context_congs) = extraction_thms thy
val tych = Thry.typecheck thy
val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
- val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
+ val Const(@{const_name "All"},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
Rtype)
val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
--- a/src/HOL/Tools/TFL/usyntax.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Thu Aug 19 11:02:14 2010 +0200
@@ -159,7 +159,7 @@
fun mk_imp{ant,conseq} =
- let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name "op -->"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[ant,conseq])
end;
@@ -171,24 +171,24 @@
fun mk_forall (r as {Bvar,Body}) =
let val ty = type_of Bvar
- val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT)
+ val c = Const(@{const_name "All"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
in list_comb(c,[mk_abs r])
end;
fun mk_exists (r as {Bvar,Body}) =
let val ty = type_of Bvar
- val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT)
+ val c = Const(@{const_name "Ex"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
in list_comb(c,[mk_abs r])
end;
fun mk_conj{conj1,conj2} =
- let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name "op &"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[conj1,conj2])
end;
fun mk_disj{disj1,disj2} =
- let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name "op |"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[disj1,disj2])
end;
@@ -244,25 +244,25 @@
end
| dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction";
-fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
+fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
| dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
-fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
+fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
| dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
-fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a)
+fun dest_forall(Const(@{const_name "All"},_) $ (a as Abs _)) = fst (dest_abs [] a)
| dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
-fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a)
+fun dest_exists(Const(@{const_name "Ex"},_) $ (a as Abs _)) = fst (dest_abs [] a)
| dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
fun dest_neg(Const("not",_) $ M) = M
| dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
-fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
+fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
| dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
-fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
+fun dest_disj(Const(@{const_name "op |"},_) $ M $ N) = {disj1=M, disj2=N}
| dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
fun mk_pair{fst,snd} =
@@ -402,6 +402,6 @@
| is_WFR _ = false;
fun ARB ty = mk_select{Bvar=Free("v",ty),
- Body=Const("True",HOLogic.boolT)};
+ Body=Const(@{const_name "True"},HOLogic.boolT)};
end;
--- a/src/HOL/Tools/choice_specification.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Thu Aug 19 11:02:14 2010 +0200
@@ -24,7 +24,7 @@
fun mk_definitional [] arg = arg
| mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
case HOLogic.dest_Trueprop (concl_of thm) of
- Const("Ex",_) $ P =>
+ Const(@{const_name "Ex"},_) $ P =>
let
val ctype = domain_type (type_of P)
val cname_full = Sign.intern_const thy cname
@@ -51,7 +51,7 @@
end
| process ((thname,cname,covld)::cos) (thy,tm) =
case tm of
- Const("Ex",_) $ P =>
+ Const(@{const_name "Ex"},_) $ P =>
let
val ctype = domain_type (type_of P)
val cname_full = Sign.intern_const thy cname
--- a/src/HOL/Tools/cnf_funcs.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Thu Aug 19 11:02:14 2010 +0200
@@ -93,19 +93,19 @@
val cnftac_eq_imp = @{lemma "[| P = Q; P |] ==> Q" by auto};
-fun is_atom (Const ("False", _)) = false
- | is_atom (Const ("True", _)) = false
- | is_atom (Const ("op &", _) $ _ $ _) = false
- | is_atom (Const ("op |", _) $ _ $ _) = false
- | is_atom (Const ("op -->", _) $ _ $ _) = false
- | is_atom (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
- | is_atom (Const ("Not", _) $ _) = false
+fun is_atom (Const (@{const_name "False"}, _)) = false
+ | is_atom (Const (@{const_name "True"}, _)) = false
+ | is_atom (Const (@{const_name "op &"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name "op |"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
+ | is_atom (Const (@{const_name "Not"}, _) $ _) = false
| is_atom _ = true;
-fun is_literal (Const ("Not", _) $ x) = is_atom x
+fun is_literal (Const (@{const_name "Not"}, _) $ x) = is_atom x
| is_literal x = is_atom x;
-fun is_clause (Const ("op |", _) $ x $ y) = is_clause x andalso is_clause y
+fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
| is_clause x = is_literal x;
(* ------------------------------------------------------------------------- *)
@@ -118,7 +118,7 @@
fun clause_is_trivial c =
let
(* Term.term -> Term.term *)
- fun dual (Const ("Not", _) $ x) = x
+ fun dual (Const (@{const_name "Not"}, _) $ x) = x
| dual x = HOLogic.Not $ x
(* Term.term list -> bool *)
fun has_duals [] = false
@@ -184,28 +184,28 @@
(* Theory.theory -> Term.term -> Thm.thm *)
-fun make_nnf_thm thy (Const ("op &", _) $ x $ y) =
+fun make_nnf_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy y
in
conj_cong OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("op |", _) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy y
in
disj_cong OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("op -->", _) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name "op -->"}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy y
in
make_nnf_imp OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -214,32 +214,32 @@
in
make_nnf_iff OF [thm1, thm2, thm3, thm4]
end
- | make_nnf_thm thy (Const ("Not", _) $ Const ("False", _)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "False"}, _)) =
make_nnf_not_false
- | make_nnf_thm thy (Const ("Not", _) $ Const ("True", _)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "True"}, _)) =
make_nnf_not_true
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op &", _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_conj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op |", _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_disj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op -->", _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_imp OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -248,7 +248,7 @@
in
make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("Not", _) $ x)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "Not"}, _) $ x)) =
let
val thm1 = make_nnf_thm thy x
in
@@ -276,7 +276,7 @@
(* Theory.theory -> Term.term -> Thm.thm *)
-fun simp_True_False_thm thy (Const ("op &", _) $ x $ y) =
+fun simp_True_False_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
let
val thm1 = simp_True_False_thm thy x
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -298,7 +298,7 @@
conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *)
end
end
- | simp_True_False_thm thy (Const ("op |", _) $ x $ y) =
+ | simp_True_False_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
let
val thm1 = simp_True_False_thm thy x
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -334,24 +334,24 @@
fun make_cnf_thm thy t =
let
(* Term.term -> Thm.thm *)
- fun make_cnf_thm_from_nnf (Const ("op &", _) $ x $ y) =
+ fun make_cnf_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) =
let
val thm1 = make_cnf_thm_from_nnf x
val thm2 = make_cnf_thm_from_nnf y
in
conj_cong OF [thm1, thm2]
end
- | make_cnf_thm_from_nnf (Const ("op |", _) $ x $ y) =
+ | make_cnf_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
let
(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
- fun make_cnf_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
+ fun make_cnf_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
let
val thm1 = make_cnf_disj_thm x1 y'
val thm2 = make_cnf_disj_thm x2 y'
in
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
end
- | make_cnf_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
+ | make_cnf_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
let
val thm1 = make_cnf_disj_thm x' y1
val thm2 = make_cnf_disj_thm x' y2
@@ -403,34 +403,34 @@
val var_id = Unsynchronized.ref 0 (* properly initialized below *)
fun new_free () =
Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
- fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) : thm =
+ fun make_cnfx_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) : thm =
let
val thm1 = make_cnfx_thm_from_nnf x
val thm2 = make_cnfx_thm_from_nnf y
in
conj_cong OF [thm1, thm2]
end
- | make_cnfx_thm_from_nnf (Const ("op |", _) $ x $ y) =
+ | make_cnfx_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
if is_clause x andalso is_clause y then
inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
else if is_literal y orelse is_literal x then let
(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
(* almost in CNF, and x' or y' is a literal *)
- fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
+ fun make_cnfx_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
let
val thm1 = make_cnfx_disj_thm x1 y'
val thm2 = make_cnfx_disj_thm x2 y'
in
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
end
- | make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
+ | make_cnfx_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
let
val thm1 = make_cnfx_disj_thm x' y1
val thm2 = make_cnfx_disj_thm x' y2
in
make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
end
- | make_cnfx_disj_thm (Const ("Ex", _) $ x') y' =
+ | make_cnfx_disj_thm (Const (@{const_name "Ex"}, _) $ x') y' =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *)
val var = new_free ()
@@ -441,7 +441,7 @@
in
iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
end
- | make_cnfx_disj_thm x' (Const ("Ex", _) $ y') =
+ | make_cnfx_disj_thm x' (Const (@{const_name "Ex"}, _) $ y') =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *)
val var = new_free ()
--- a/src/HOL/Tools/groebner.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/groebner.ML Thu Aug 19 11:02:14 2010 +0200
@@ -395,7 +395,7 @@
fun refute_disj rfn tm =
case term_of tm of
- Const("op |",_)$l$r =>
+ Const(@{const_name "op |"},_)$l$r =>
compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
| _ => rfn tm ;
@@ -405,11 +405,11 @@
val mk_comb = capply;
fun is_neg t =
case term_of t of
- (Const("Not",_)$p) => true
+ (Const(@{const_name "Not"},_)$p) => true
| _ => false;
fun is_eq t =
case term_of t of
- (Const("op =",_)$_$_) => true
+ (Const(@{const_name "op ="},_)$_$_) => true
| _ => false;
fun end_itlist f l =
@@ -430,14 +430,14 @@
val strip_exists =
let fun h (acc, t) =
case (term_of t) of
- Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
+ Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end;
fun is_forall t =
case term_of t of
- (Const("All",_)$Abs(_,_,_)) => true
+ (Const(@{const_name "All"},_)$Abs(_,_,_)) => true
| _ => false;
val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
@@ -522,7 +522,7 @@
fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
fun choose v th th' = case concl_of th of
- @{term Trueprop} $ (Const("Ex",_)$_) =>
+ @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) =>
let
val p = (funpow 2 Thm.dest_arg o cprop_of) th
val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
@@ -923,15 +923,15 @@
fun find_term bounds tm =
(case term_of tm of
- Const ("op =", T) $ _ $ _ =>
+ Const (@{const_name "op ="}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else dest_arg tm
- | Const ("Not", _) $ _ => find_term bounds (dest_arg tm)
- | Const ("All", _) $ _ => find_body bounds (dest_arg tm)
- | Const ("Ex", _) $ _ => find_body bounds (dest_arg tm)
- | Const ("op &", _) $ _ $ _ => find_args bounds tm
- | Const ("op |", _) $ _ $ _ => find_args bounds tm
- | Const ("op -->", _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "Not"}, _) $ _ => find_term bounds (dest_arg tm)
+ | Const (@{const_name "All"}, _) $ _ => find_body bounds (dest_arg tm)
+ | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (dest_arg tm)
+ | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
| @{term "op ==>"} $_$_ => find_args bounds tm
| Const("op ==",_)$_$_ => find_args bounds tm
| @{term Trueprop}$_ => find_term bounds (dest_arg tm)
@@ -985,7 +985,7 @@
local
fun lhs t = case term_of t of
- Const("op =",_)$_$_ => Thm.dest_arg1 t
+ Const(@{const_name "op ="},_)$_$_ => Thm.dest_arg1 t
| _=> raise CTERM ("ideal_tac - lhs",[t])
fun exitac NONE = no_tac
| exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
--- a/src/HOL/Tools/lin_arith.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Aug 19 11:02:14 2010 +0200
@@ -46,12 +46,12 @@
val mk_Trueprop = HOLogic.mk_Trueprop;
fun atomize thm = case Thm.prop_of thm of
- Const ("Trueprop", _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
+ Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
| _ => [thm];
-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)
+fun neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
+ | neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ t) = TP $ (HOLogic.Not $t)
| neg_prop t = raise TERM ("neg_prop", [t]);
fun is_False thm =
@@ -258,10 +258,10 @@
| negate NONE = NONE;
fun decomp_negation data
- ((Const ("Trueprop", _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
+ ((Const (@{const_name "Trueprop"}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
decomp_typecheck data (T, (rel, lhs, rhs))
- | decomp_negation data ((Const ("Trueprop", _)) $
- (Const ("Not", _) $ (Const (rel, T) $ lhs $ rhs))) =
+ | decomp_negation data ((Const (@{const_name "Trueprop"}, _)) $
+ (Const (@{const_name "Not"}, _) $ (Const (rel, T) $ lhs $ rhs))) =
negate (decomp_typecheck data (T, (rel, lhs, rhs)))
| decomp_negation data _ =
NONE;
@@ -273,7 +273,7 @@
in decomp_negation (thy, discrete, inj_consts) end;
fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T
- | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
+ | domain_is_nat (_ $ (Const (@{const_name "Not"}, _) $ (Const (_, T) $ _ $ _))) = nT T
| domain_is_nat _ = false;
@@ -428,7 +428,7 @@
val t2' = incr_boundvars 1 t2
val t1_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
- val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_plus_d = Const (@{const_name "op ="}, 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)
@@ -448,7 +448,7 @@
(map (incr_boundvars 1) rev_terms)
val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms
val t1' = incr_boundvars 1 t1
- val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
+ val t1_eq_nat_n = Const (@{const_name "op ="}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
(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
@@ -472,13 +472,13 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const ("op =",
+ val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(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)
@@ -504,13 +504,13 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const ("op =",
+ val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(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)
@@ -542,7 +542,7 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -556,7 +556,7 @@
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(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)
@@ -596,7 +596,7 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -610,7 +610,7 @@
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(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)
@@ -659,7 +659,7 @@
fun negated_term_occurs_positively (terms : term list) : bool =
List.exists
- (fn (Trueprop $ (Const ("Not", _) $ t)) =>
+ (fn (Trueprop $ (Const (@{const_name "Not"}, _) $ t)) =>
member Pattern.aeconv terms (Trueprop $ t)
| _ => false)
terms;
--- a/src/HOL/Tools/meson.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Aug 19 11:02:14 2010 +0200
@@ -149,21 +149,21 @@
(*Are any of the logical connectives in "bs" present in the term?*)
fun has_conns bs =
let fun has (Const(a,_)) = false
- | has (Const("Trueprop",_) $ p) = has p
- | has (Const("Not",_) $ p) = has p
- | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
- | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
- | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
- | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
+ | has (Const(@{const_name "Trueprop"},_) $ p) = has p
+ | has (Const(@{const_name "Not"},_) $ p) = has p
+ | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
+ | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
+ | has (Const(@{const_name "All"},_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
+ | has (Const(@{const_name "Ex"},_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
| has _ = false
in has end;
(**** Clause handling ****)
-fun literals (Const("Trueprop",_) $ P) = literals P
- | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
- | literals (Const("Not",_) $ P) = [(false,P)]
+fun literals (Const(@{const_name "Trueprop"},_) $ P) = literals P
+ | literals (Const(@{const_name "op |"},_) $ P $ Q) = literals P @ literals Q
+ | literals (Const(@{const_name "Not"},_) $ P) = [(false,P)]
| literals P = [(true,P)];
(*number of literals in a term*)
@@ -172,16 +172,16 @@
(*** Tautology Checking ***)
-fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
+fun signed_lits_aux (Const (@{const_name "op |"}, _) $ P $ Q) (poslits, neglits) =
signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
- | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
+ | signed_lits_aux (Const(@{const_name "Not"},_) $ P) (poslits, neglits) = (poslits, P::neglits)
| signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
(*Literals like X=X are tautologous*)
-fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
- | taut_poslit (Const("True",_)) = true
+fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
+ | taut_poslit (Const(@{const_name "True"},_)) = true
| taut_poslit _ = false;
fun is_taut th =
@@ -208,18 +208,18 @@
fun refl_clause_aux 0 th = th
| refl_clause_aux n th =
case HOLogic.dest_Trueprop (concl_of th) of
- (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
+ (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
- | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
+ | (Const (@{const_name "op |"}, _) $ (Const(@{const_name "Not"},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
if eliminable(t,u)
then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
- | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
+ | (Const (@{const_name "op |"}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
| _ => (*not a disjunction*) th;
-fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
+fun notequal_lits_count (Const (@{const_name "op |"}, _) $ P $ Q) =
notequal_lits_count P + notequal_lits_count Q
- | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
+ | notequal_lits_count (Const(@{const_name "Not"},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
| notequal_lits_count _ = 0;
(*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -266,26 +266,26 @@
fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
(*Estimate the number of clauses in order to detect infeasible theorems*)
- fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
- | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
- | signed_nclauses b (Const("op &",_) $ t $ u) =
+ fun signed_nclauses b (Const(@{const_name "Trueprop"},_) $ t) = signed_nclauses b t
+ | signed_nclauses b (Const(@{const_name "Not"},_) $ t) = signed_nclauses (not b) t
+ | signed_nclauses b (Const(@{const_name "op &"},_) $ t $ u) =
if b then sum (signed_nclauses b t) (signed_nclauses b u)
else prod (signed_nclauses b t) (signed_nclauses b u)
- | signed_nclauses b (Const("op |",_) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
if b then prod (signed_nclauses b t) (signed_nclauses b u)
else sum (signed_nclauses b t) (signed_nclauses b u)
- | signed_nclauses b (Const("op -->",_) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name "op -->"},_) $ t $ u) =
if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
else sum (signed_nclauses (not b) t) (signed_nclauses b u)
- | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
(prod (signed_nclauses (not b) u) (signed_nclauses b t))
else sum (prod (signed_nclauses b t) (signed_nclauses b u))
(prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
else 1
- | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
- | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
+ | signed_nclauses b (Const(@{const_name "Ex"}, _) $ Abs (_,_,t)) = signed_nclauses b t
+ | signed_nclauses b (Const(@{const_name "All"},_) $ Abs (_,_,t)) = signed_nclauses b t
| signed_nclauses _ _ = 1; (* literal *)
in
signed_nclauses true t >= max_cl
@@ -296,7 +296,7 @@
local
val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
val spec_varT = #T (Thm.rep_cterm spec_var);
- fun name_of (Const ("All", _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
+ fun name_of (Const (@{const_name "All"}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
in
fun freeze_spec th ctxt =
let
@@ -334,15 +334,15 @@
else if not (has_conns ["All","Ex","op &"] (prop_of th))
then nodups ctxt th :: ths (*no work to do, terminate*)
else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
- Const ("op &", _) => (*conjunction*)
+ Const (@{const_name "op &"}, _) => (*conjunction*)
cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
- | Const ("All", _) => (*universal quantifier*)
+ | Const (@{const_name "All"}, _) => (*universal quantifier*)
let val (th',ctxt') = freeze_spec th (!ctxtr)
in ctxtr := ctxt'; cnf_aux (th', ths) end
- | Const ("Ex", _) =>
+ | Const (@{const_name "Ex"}, _) =>
(*existential quantifier: Insert Skolem functions*)
cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
- | Const ("op |", _) =>
+ | Const (@{const_name "op |"}, _) =>
(*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
all combinations of converting P, Q to CNF.*)
let val tac =
@@ -365,8 +365,8 @@
(**** Generation of contrapositives ****)
-fun is_left (Const ("Trueprop", _) $
- (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
+fun is_left (Const (@{const_name "Trueprop"}, _) $
+ (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
| is_left _ = false;
(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -429,8 +429,8 @@
fun rigid t = not (is_Var (head_of t));
-fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
- | ok4horn (Const ("Trueprop",_) $ t) = rigid t
+fun ok4horn (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
+ | ok4horn (Const (@{const_name "Trueprop"},_) $ t) = rigid t
| ok4horn _ = false;
(*Create a meta-level Horn clause*)
@@ -464,7 +464,7 @@
(***** MESON PROOF PROCEDURE *****)
-fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
+fun rhyps (Const("==>",_) $ (Const(@{const_name "Trueprop"},_) $ A) $ phi,
As) = rhyps(phi, A::As)
| rhyps (_, As) = As;
@@ -509,8 +509,8 @@
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
not_impD, not_iffD, not_allD, not_exD, not_notD];
-fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
- | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
+fun ok4nnf (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ t)) = rigid t
+ | ok4nnf (Const (@{const_name "Trueprop"},_) $ t) = rigid t
| ok4nnf _ = false;
fun make_nnf1 ctxt th =
--- a/src/HOL/Tools/numeral_simprocs.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Thu Aug 19 11:02:14 2010 +0200
@@ -676,7 +676,7 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
in SOME (mk_meta_eq th) end
- | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ | Const(@{const_name "op ="},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
@@ -697,7 +697,7 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name "op ="},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
--- a/src/HOL/Tools/prop_logic.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML Thu Aug 19 11:02:14 2010 +0200
@@ -391,20 +391,20 @@
next_idx_is_valid := true;
Unsynchronized.inc next_idx
)
- fun aux (Const ("True", _)) table =
+ fun aux (Const (@{const_name "True"}, _)) table =
(True, table)
- | aux (Const ("False", _)) table =
+ | aux (Const (@{const_name "False"}, _)) table =
(False, table)
- | aux (Const ("Not", _) $ x) table =
+ | aux (Const (@{const_name "Not"}, _) $ x) table =
apfst Not (aux x table)
- | aux (Const ("op |", _) $ x $ y) table =
+ | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1
in
(Or (fm1, fm2), table2)
end
- | aux (Const ("op &", _) $ x $ y) table =
+ | aux (Const (@{const_name "op &"}, _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1
--- a/src/HOL/Tools/quickcheck_generators.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu Aug 19 11:02:14 2010 +0200
@@ -342,7 +342,7 @@
val bound_max = length Ts - 1;
val bounds = map_index (fn (i, ty) =>
(2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
- fun strip_imp (Const("op -->",_) $ A $ B) = apfst (cons A) (strip_imp B)
+ fun strip_imp (Const(@{const_name "op -->"},_) $ A $ B) = apfst (cons A) (strip_imp B)
| strip_imp A = ([], A)
val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
--- a/src/HOL/Tools/sat_funcs.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Thu Aug 19 11:02:14 2010 +0200
@@ -217,7 +217,7 @@
(* Thm.cterm -> int option *)
fun index_of_literal chyp = (
case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
- (Const ("Not", _) $ atom) =>
+ (Const (@{const_name "Not"}, _) $ atom) =>
SOME (~ (the (Termtab.lookup atom_table atom)))
| atom =>
SOME (the (Termtab.lookup atom_table atom))
--- a/src/HOL/ex/SVC_Oracle.thy Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Thu Aug 19 11:02:14 2010 +0200
@@ -88,18 +88,18 @@
else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
else replace (c $ x $ y) (*non-numeric comparison*)
(*abstraction of a formula*)
- and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
- | fm ((c as Const("True", _))) = c
- | fm ((c as Const("False", _))) = c
- | fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name "Not"}, _)) $ p) = c $ (fm p)
+ | fm ((c as Const(@{const_name "True"}, _))) = c
+ | fm ((c as Const(@{const_name "False"}, _))) = c
+ | fm (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
(*entry point, and abstraction of a meta-formula*)
- fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
+ fun mt ((c as Const(@{const_name "Trueprop"}, _)) $ p) = c $ (fm p)
| mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
| mt t = fm t (*it might be a formula*)
in (list_all (params, mt body), !pairs) end;
--- a/src/HOL/ex/svc_funcs.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML Thu Aug 19 11:02:14 2010 +0200
@@ -89,13 +89,13 @@
let fun tag t =
let val (c,ts) = strip_comb t
in case c of
- Const("op &", _) => apply c (map tag ts)
- | Const("op |", _) => apply c (map tag ts)
- | Const("op -->", _) => apply c (map tag ts)
- | Const("Not", _) => apply c (map tag ts)
- | Const("True", _) => (c, false)
- | Const("False", _) => (c, false)
- | Const("op =", Type ("fun", [T,_])) =>
+ Const(@{const_name "op &"}, _) => apply c (map tag ts)
+ | Const(@{const_name "op |"}, _) => apply c (map tag ts)
+ | Const(@{const_name "op -->"}, _) => apply c (map tag ts)
+ | Const(@{const_name "Not"}, _) => apply c (map tag ts)
+ | Const(@{const_name "True"}, _) => (c, false)
+ | Const(@{const_name "False"}, _) => (c, false)
+ | Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
if T = HOLogic.boolT then
(*biconditional: with int/nat comparisons below?*)
let val [t1,t2] = ts
@@ -183,16 +183,16 @@
| tm t = Int (lit t)
handle Match => var (t,[])
(*translation of a formula*)
- and fm pos (Const("op &", _) $ p $ q) =
+ and fm pos (Const(@{const_name "op &"}, _) $ p $ q) =
Buildin("AND", [fm pos p, fm pos q])
- | fm pos (Const("op |", _) $ p $ q) =
+ | fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
Buildin("OR", [fm pos p, fm pos q])
- | fm pos (Const("op -->", _) $ p $ q) =
+ | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
Buildin("=>", [fm (not pos) p, fm pos q])
- | fm pos (Const("Not", _) $ p) =
+ | fm pos (Const(@{const_name "Not"}, _) $ p) =
Buildin("NOT", [fm (not pos) p])
- | fm pos (Const("True", _)) = TrueExpr
- | fm pos (Const("False", _)) = FalseExpr
+ | fm pos (Const(@{const_name "True"}, _)) = TrueExpr
+ | fm pos (Const(@{const_name "False"}, _)) = FalseExpr
| fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
(*polarity doesn't matter*)
Buildin("=", [fm pos p, fm pos q])
@@ -200,7 +200,7 @@
Buildin("AND", (*unfolding uses both polarities*)
[Buildin("=>", [fm (not pos) p, fm pos q]),
Buildin("=>", [fm (not pos) q, fm pos p])])
- | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ x $ y) =
let val tx = tm x and ty = tm y
in if pos orelse T = HOLogic.realT then
Buildin("=", [tx, ty])
@@ -225,7 +225,7 @@
else fail t
| fm pos t = var(t,[]);
(*entry point, and translation of a meta-formula*)
- fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)
+ fun mt pos ((c as Const(@{const_name "Trueprop"}, _)) $ p) = fm pos (iff_tag p)
| mt pos ((c as Const("==>", _)) $ p $ q) =
Buildin("=>", [mt (not pos) p, mt pos q])
| mt pos t = fm pos (iff_tag t) (*it might be a formula*)
--- a/src/HOLCF/Tools/Domain/domain_library.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Thu Aug 19 11:02:14 2010 +0200
@@ -121,8 +121,8 @@
val r_inst = read_instantiate ctxt;
fun at thm =
case concl_of thm of
- _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
- | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
+ _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ | _$(Const(@{const_name "All"} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
| _ => [thm];
in map zero_var_indexes (at thm) end;