--- a/src/HOL/Import/proof_kernel.ML Thu Aug 19 16:08:53 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Thu Aug 19 16:08:54 2010 +0200
@@ -1006,7 +1006,7 @@
local
val th = thm "not_def"
val thy = theory_of_thm th
- val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},HOLogic.boolT-->propT)))
+ val pp = Thm.reflexive (cterm_of thy (Const(@{const_name Trueprop},HOLogic.boolT-->propT)))
in
val not_elim_thm = Thm.combination pp th
end
@@ -1052,9 +1052,9 @@
val c = prop_of th3
val vname = fst(dest_Free v)
val (cold,cnew) = case c of
- tpc $ (Const(@{const_name "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(@{const_name "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
@@ -1204,7 +1204,8 @@
fun non_trivial_term_consts t = fold_aterms
(fn Const (c, _) =>
- if c = "Trueprop" orelse c = "All" orelse c = "op -->" orelse c = "op &" orelse c = "op ="
+ if c = @{const_name Trueprop} orelse c = @{const_name All}
+ orelse c = @{const_name "op -->"} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
then I else insert (op =) c
| _ => I) t [];
@@ -1212,12 +1213,12 @@
let
fun add_consts (Const (c, _), cs) =
(case c of
- "op =" => insert (op =) "==" cs
- | "op -->" => insert (op =) "==>" cs
- | "All" => cs
+ @{const_name "op ="} => insert (op =) "==" cs
+ | @{const_name "op -->"} => insert (op =) "==>" cs
+ | @{const_name All} => cs
| "all" => cs
- | "op &" => cs
- | "Trueprop" => cs
+ | @{const_name "op &"} => cs
+ | @{const_name Trueprop} => cs
| _ => insert (op =) c cs)
| add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
| add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
@@ -1653,7 +1654,7 @@
val cwit = cterm_of thy wit'
val cty = ctyp_of_term cwit
val a = case ex' of
- (Const(@{const_name "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)
@@ -1686,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(@{const_name "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)
@@ -1772,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(@{const_name "Not"},HOLogic.boolT-->HOLogic.boolT) $ tm')) th
+ val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name Not},HOLogic.boolT-->HOLogic.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)
@@ -1859,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(@{const_name "op -->"},_) $ a $ Const(@{const_name "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
@@ -1876,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(@{const_name "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
@@ -1995,7 +1996,7 @@
("x",dT,body $ Bound 0)
end
handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
- fun dest_exists (Const(@{const_name "Ex"},_) $ abody) =
+ fun dest_exists (Const(@{const_name Ex},_) $ abody) =
dest_eta_abs abody
| dest_exists tm =
raise ERR "new_specification" "Bad existential formula"
@@ -2081,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(@{const_name "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
@@ -2107,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(@{const_name "Ex"},exT) $ P =>
+ Const(@{const_name Ex},exT) $ P =>
let
val PT = domain_type exT
in
@@ -2156,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(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
+ _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
| _ => raise ERR "type_introduction" "Bad type definition theorem"
val tfrees = OldTerm.term_tfrees c
val tnames = sort_strings (map fst tfrees)
--- a/src/HOL/Prolog/prolog.ML Thu Aug 19 16:08:53 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML Thu Aug 19 16:08:54 2010 +0200
@@ -10,17 +10,17 @@
exception not_HOHH;
fun isD t = case t of
- Const(@{const_name "Trueprop"},_)$t => isD t
+ 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(@{const_name "All"},_)$Abs(s,_,t) => isD t
+ | Const(@{const_name All},_)$Abs(s,_,t) => isD t
| Const("all",_)$Abs(s,_,t) => isD t
| Const(@{const_name "op |"},_)$_$_ => false
- | Const(@{const_name "Ex"} ,_)$_ => false
- | Const("not",_)$_ => false
- | Const(@{const_name "True"},_) => false
- | Const(@{const_name "False"},_) => false
+ | Const(@{const_name Ex} ,_)$_ => false
+ | Const(@{const_name Not},_)$_ => 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(@{const_name "Trueprop"},_)$t => isG t
+ 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(@{const_name "All"},_)$Abs(_,_,t) => isG t
+ | Const(@{const_name All},_)$Abs(_,_,t) => isG t
| Const("all",_)$Abs(_,_,t) => isG t
- | Const(@{const_name "Ex"} ,_)$Abs(_,_,t) => isG t
- | Const(@{const_name "True"},_) => true
- | Const("not",_)$_ => false
- | Const(@{const_name "False"},_) => false
+ | Const(@{const_name Ex} ,_)$Abs(_,_,t) => isG t
+ | Const(@{const_name True},_) => true
+ | Const(@{const_name Not},_)$_ => false
+ | Const(@{const_name False},_) => false
| _ (* atom *) => true;
val check_HOHH_tac1 = PRIMITIVE (fn thm =>
@@ -51,7 +51,7 @@
fun atomizeD ctxt thm = let
fun at thm = case concl_of thm of
- _$(Const(@{const_name "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(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const(@{const_name "op -->"},_)$_$_) => at(thm RS mp)
@@ -71,7 +71,7 @@
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(@{const_name "All"},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,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);
(*
@@ -79,7 +79,7 @@
| rep_goal (Const ("==>",_)$s$t) =
(case rep_goal t of (l,t) => (s::l,t))
| rep_goal t = ([] ,t);
- val (prems, Const(@{const_name "Trueprop"}, _)$concl) = rep_goal
+ val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
(#3(dest_state (st,i)));
*)
val subgoal = #3(Thm.dest_state (st,i));
--- a/src/HOL/Tools/Function/termination.ML Thu Aug 19 16:08:53 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML Thu Aug 19 16:08:54 2010 +0200
@@ -149,7 +149,7 @@
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
- = Term.strip_qnt_body "Ex" c
+ = Term.strip_qnt_body @{const_name Ex} c
in cons r o cons l end
in
mk_skel (fold collect_pats cs [])
@@ -182,11 +182,11 @@
fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
val (sk, _, _, _, _) = D
- val vs = Term.strip_qnt_vars "Ex" c
+ val vs = Term.strip_qnt_vars @{const_name Ex} c
(* FIXME: throw error "dest_call" for malformed terms *)
val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
- = Term.strip_qnt_body "Ex" c
+ = Term.strip_qnt_body @{const_name Ex} c
val (p, l') = dest_inj sk l
val (q, r') = dest_inj sk r
in
--- a/src/HOL/Tools/meson.ML Thu Aug 19 16:08:53 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Aug 19 16:08:54 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(@{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 (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 @{const_name "op |"} orelse has p orelse has q
+ | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs @{const_name "op &"} orelse has p orelse has q
+ | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
+ | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
| has _ = false
in has end;
(**** Clause handling ****)
-fun literals (Const(@{const_name "Trueprop"},_) $ P) = literals 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 (Const(@{const_name Not},_) $ P) = [(false,P)]
| literals P = [(true,P)];
(*number of literals in a term*)
@@ -174,14 +174,14 @@
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(@{const_name "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(@{const_name "op ="},_) $ t $ u) = t aconv u
- | taut_poslit (Const(@{const_name "True"},_)) = true
+ | taut_poslit (Const(@{const_name True},_)) = true
| taut_poslit _ = false;
fun is_taut th =
@@ -210,7 +210,7 @@
case HOLogic.dest_Trueprop (concl_of th) of
(Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
- | (Const (@{const_name "op |"}, _) $ (Const(@{const_name "Not"},_) $ (Const(@{const_name "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*)
@@ -219,7 +219,7 @@
fun notequal_lits_count (Const (@{const_name "op |"}, _) $ P $ Q) =
notequal_lits_count P + notequal_lits_count Q
- | notequal_lits_count (Const(@{const_name "Not"},_) $ (Const(@{const_name "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,8 +266,8 @@
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(@{const_name "Trueprop"},_) $ t) = signed_nclauses b t
- | signed_nclauses b (Const(@{const_name "Not"},_) $ t) = signed_nclauses (not b) t
+ 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)
@@ -284,8 +284,8 @@
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(@{const_name "Ex"}, _) $ Abs (_,_,t)) = signed_nclauses b t
- | signed_nclauses b (Const(@{const_name "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 (@{const_name "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
@@ -314,8 +314,7 @@
(*Any need to extend this list with
"HOL.type_class","HOL.eq_class","Pure.term"?*)
-val has_meta_conn =
- exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
+val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
fun apply_skolem_theorem (th, rls) =
let
@@ -331,15 +330,15 @@
let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
- else if not (has_conns ["All","Ex","op &"] (prop_of th))
+ else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name "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 (@{const_name "op &"}, _) => (*conjunction*)
cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
- | Const (@{const_name "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 (@{const_name "Ex"}, _) =>
+ | Const (@{const_name Ex}, _) =>
(*existential quantifier: Insert Skolem functions*)
cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
| Const (@{const_name "op |"}, _) =>
@@ -365,7 +364,7 @@
(**** Generation of contrapositives ****)
-fun is_left (Const (@{const_name "Trueprop"}, _) $
+fun is_left (Const (@{const_name Trueprop}, _) $
(Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
| is_left _ = false;
@@ -401,8 +400,9 @@
(*Is the string the name of a connective? Really only | and Not can remain,
since this code expects to be called on a clause form.*)
val is_conn = member (op =)
- ["Trueprop", "op &", "op |", "op -->", "Not",
- "All", "Ex", @{const_name Ball}, @{const_name Bex}];
+ [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
+ @{const_name "op -->"}, @{const_name Not},
+ @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
(*True if the term contains a function--not a logical connective--where the type
of any argument contains bool.*)
@@ -420,7 +420,7 @@
(*Returns false if any Vars in the theorem mention type bool.
Also rejects functions whose arguments are Booleans or other functions.*)
fun is_fol_term thy t =
- Term.is_first_order ["all","All","Ex"] t andalso
+ Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso
not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
| _ => false) t orelse
has_bool_arg_const t orelse
@@ -429,8 +429,8 @@
fun rigid t = not (is_Var (head_of t));
-fun ok4horn (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
- | ok4horn (Const (@{const_name "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(@{const_name "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 (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ t)) = rigid t
- | ok4nnf (Const (@{const_name "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 =
@@ -546,7 +546,7 @@
(*Pull existential quantifiers to front. This accomplishes Skolemization for
clauses that arise from a subgoal.*)
fun skolemize1 ctxt th =
- if not (has_conns ["Ex"] (prop_of th)) then th
+ if not (has_conns [@{const_name Ex}] (prop_of th)) then th
else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2,
disj_exD, disj_exD1, disj_exD2])))
handle THM ("tryres", _, _) =>
--- a/src/HOLCF/Tools/Domain/domain_library.ML Thu Aug 19 16:08:53 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Thu Aug 19 16:08:54 2010 +0200
@@ -122,7 +122,7 @@
fun at thm =
case concl_of thm of
_$(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))
+ | _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
| _ => [thm];
in map zero_var_indexes (at thm) end;
@@ -185,7 +185,7 @@
fun mk_lam (x,T) = Abs(x,dummyT,T);
fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
fun mk_ex (x,P) = mk_exists (x,dummyT,P);
-fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
+fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
end
fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)