# HG changeset patch # User haftmann # Date 1282208534 -7200 # Node ID d0385f2764d893dc05b7001ac844c885b532c096 # Parent dea0d2cca822ba80b10bbe7487f7d60669f4f93b use antiquotations for remaining unqualified constants in HOL diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Decision_Procs/Approximation.thy --- 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]) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Decision_Procs/Cooper.thy --- 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; diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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 \"}, @{term "op \"}] 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Decision_Procs/Ferrack.thy --- 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); diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Decision_Procs/MIR.thy --- 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); diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Decision_Procs/cooper_tac.ML --- 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, diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Decision_Procs/ferrack_tac.ML --- 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" ^ diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Decision_Procs/ferrante_rackoff.ML --- 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) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Decision_Procs/langford.ML --- 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)) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Decision_Procs/mir_tac.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Import/proof_kernel.ML --- 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) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Import/shuffler.ML --- 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 _ *) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Library/Eval_Witness.thy --- 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); diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Library/positivstellensatz.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Library/reflection.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Nominal/nominal_datatype.ML --- 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)); diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Nominal/nominal_inductive.ML --- 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, diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Nominal/nominal_inductive2.ML --- 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, diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Nominal/nominal_thmdecls.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Prolog/prolog.ML --- 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)); diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Statespace/distinct_tree_prover.ML --- 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) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Statespace/state_fun.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Statespace/state_space.ML --- 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) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/TLA/Intensional.thy --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Function/function_core.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Function/termination.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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 = diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- 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} diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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); diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Qelim/cooper.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- 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) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/TFL/post.ML --- 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??*) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/TFL/rules.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/TFL/tfl.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/TFL/usyntax.ML --- 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; diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/choice_specification.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/cnf_funcs.ML --- 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 () diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/groebner.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/lin_arith.ML --- 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; diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/meson.ML --- 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 = diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/numeral_simprocs.ML --- 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] diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/prop_logic.ML --- 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 diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/quickcheck_generators.ML --- 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) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/sat_funcs.ML --- 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)) diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/ex/SVC_Oracle.thy --- 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; diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/ex/svc_funcs.ML --- 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*) diff -r dea0d2cca822 -r d0385f2764d8 src/HOLCF/Tools/Domain/domain_library.ML --- 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;