1.1 --- a/src/HOL/Import/proof_kernel.ML Thu Aug 19 10:27:12 2010 +0200
1.2 +++ b/src/HOL/Import/proof_kernel.ML Thu Aug 19 11:02:14 2010 +0200
1.3 @@ -1007,7 +1007,7 @@
1.4 local
1.5 val th = thm "not_def"
1.6 val thy = theory_of_thm th
1.7 - val pp = Thm.reflexive (cterm_of thy (Const("Trueprop",boolT-->propT)))
1.8 + val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},boolT-->propT)))
1.9 in
1.10 val not_elim_thm = Thm.combination pp th
1.11 end
1.12 @@ -1053,9 +1053,9 @@
1.13 val c = prop_of th3
1.14 val vname = fst(dest_Free v)
1.15 val (cold,cnew) = case c of
1.16 - tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) =>
1.17 + tpc $ (Const(@{const_name "All"},allT) $ Abs(oldname,ty,body)) =>
1.18 (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
1.19 - | tpc $ (Const("All",allT) $ rest) => (tpc,tpc)
1.20 + | tpc $ (Const(@{const_name "All"},allT) $ rest) => (tpc,tpc)
1.21 | _ => raise ERR "mk_GEN" "Unknown conclusion"
1.22 val th4 = Thm.rename_boundvars cold cnew th3
1.23 val res = implies_intr_hyps th4
1.24 @@ -1476,10 +1476,10 @@
1.25 fun mk_COMB th1 th2 thy =
1.26 let
1.27 val (f,g) = case concl_of th1 of
1.28 - _ $ (Const("op =",_) $ f $ g) => (f,g)
1.29 + _ $ (Const(@{const_name "op ="},_) $ f $ g) => (f,g)
1.30 | _ => raise ERR "mk_COMB" "First theorem not an equality"
1.31 val (x,y) = case concl_of th2 of
1.32 - _ $ (Const("op =",_) $ x $ y) => (x,y)
1.33 + _ $ (Const(@{const_name "op ="},_) $ x $ y) => (x,y)
1.34 | _ => raise ERR "mk_COMB" "Second theorem not an equality"
1.35 val fty = type_of f
1.36 val (fd,fr) = dom_rng fty
1.37 @@ -1521,7 +1521,7 @@
1.38 val th1 = norm_hyps th1
1.39 val th2 = norm_hyps th2
1.40 val (l,r) = case concl_of th of
1.41 - _ $ (Const("op |",_) $ l $ r) => (l,r)
1.42 + _ $ (Const(@{const_name "op |"},_) $ l $ r) => (l,r)
1.43 | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
1.44 val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
1.45 val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
1.46 @@ -1654,7 +1654,7 @@
1.47 val cwit = cterm_of thy wit'
1.48 val cty = ctyp_of_term cwit
1.49 val a = case ex' of
1.50 - (Const("Ex",_) $ a) => a
1.51 + (Const(@{const_name "Ex"},_) $ a) => a
1.52 | _ => raise ERR "EXISTS" "Argument not existential"
1.53 val ca = cterm_of thy a
1.54 val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
1.55 @@ -1687,7 +1687,7 @@
1.56 val c = HOLogic.dest_Trueprop (concl_of th2)
1.57 val cc = cterm_of thy c
1.58 val a = case concl_of th1 of
1.59 - _ $ (Const("Ex",_) $ a) => a
1.60 + _ $ (Const(@{const_name "Ex"},_) $ a) => a
1.61 | _ => raise ERR "CHOOSE" "Conclusion not existential"
1.62 val ca = cterm_of (theory_of_thm th1) a
1.63 val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
1.64 @@ -1773,7 +1773,7 @@
1.65 val (info',tm') = disamb_term_from info tm
1.66 val th = norm_hyps th
1.67 val ct = cterm_of thy tm'
1.68 - val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th
1.69 + val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name "Not"},boolT-->boolT) $ tm')) th
1.70 val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
1.71 val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
1.72 val res = HOLThm(rens_of info',res1)
1.73 @@ -1788,7 +1788,7 @@
1.74 val cv = cterm_of thy v
1.75 val th1 = implies_elim_all (beta_eta_thm th)
1.76 val (f,g) = case concl_of th1 of
1.77 - _ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
1.78 + _ $ (Const(@{const_name "op ="},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
1.79 | _ => raise ERR "mk_ABS" "Bad conclusion"
1.80 val (fd,fr) = dom_rng (type_of f)
1.81 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
1.82 @@ -1860,7 +1860,7 @@
1.83 val _ = if_debug pth hth
1.84 val th1 = implies_elim_all (beta_eta_thm th)
1.85 val a = case concl_of th1 of
1.86 - _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
1.87 + _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name "False"},_)) => a
1.88 | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
1.89 val ca = cterm_of thy a
1.90 val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
1.91 @@ -1877,7 +1877,7 @@
1.92 val _ = if_debug pth hth
1.93 val th1 = implies_elim_all (beta_eta_thm th)
1.94 val a = case concl_of th1 of
1.95 - _ $ (Const("Not",_) $ a) => a
1.96 + _ $ (Const(@{const_name "Not"},_) $ a) => a
1.97 | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
1.98 val ca = cterm_of thy a
1.99 val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
1.100 @@ -1996,7 +1996,7 @@
1.101 ("x",dT,body $ Bound 0)
1.102 end
1.103 handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
1.104 - fun dest_exists (Const("Ex",_) $ abody) =
1.105 + fun dest_exists (Const(@{const_name "Ex"},_) $ abody) =
1.106 dest_eta_abs abody
1.107 | dest_exists tm =
1.108 raise ERR "new_specification" "Bad existential formula"
1.109 @@ -2082,7 +2082,7 @@
1.110 val (HOLThm(rens,td_th)) = norm_hthm thy hth
1.111 val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
1.112 val c = case concl_of th2 of
1.113 - _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
1.114 + _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
1.115 | _ => raise ERR "new_type_definition" "Bad type definition theorem"
1.116 val tfrees = OldTerm.term_tfrees c
1.117 val tnames = map fst tfrees
1.118 @@ -2108,7 +2108,7 @@
1.119 val rew = rewrite_hol4_term (concl_of td_th) thy4
1.120 val th = Thm.equal_elim rew (Thm.transfer thy4 td_th)
1.121 val c = case HOLogic.dest_Trueprop (prop_of th) of
1.122 - Const("Ex",exT) $ P =>
1.123 + Const(@{const_name "Ex"},exT) $ P =>
1.124 let
1.125 val PT = domain_type exT
1.126 in
1.127 @@ -2157,7 +2157,7 @@
1.128 SOME (cterm_of thy t)] light_nonempty
1.129 val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
1.130 val c = case concl_of th2 of
1.131 - _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
1.132 + _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
1.133 | _ => raise ERR "type_introduction" "Bad type definition theorem"
1.134 val tfrees = OldTerm.term_tfrees c
1.135 val tnames = sort_strings (map fst tfrees)