--- 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)