--- a/src/HOL/HOL.thy Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/HOL.thy Thu Feb 25 22:32:09 2010 +0100
@@ -846,9 +846,12 @@
setup {*
let
(*prevent substitution on bool*)
- fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso
- Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false)
- (nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm;
+ fun hyp_subst_tac' i thm =
+ if i <= Thm.nprems_of thm andalso
+ Term.exists_Const
+ (fn (@{const_name "op ="}, Type (_, [T, _])) => T <> @{typ bool} | _ => false)
+ (nth (Thm.prems_of thm) (i - 1))
+ then Hypsubst.hyp_subst_tac i thm else no_tac thm;
in
Hypsubst.hypsubst_setup
#> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
@@ -1721,8 +1724,8 @@
fun eq_codegen thy defs dep thyname b t gr =
(case strip_comb t of
- (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
- | (Const ("op =", _), [t, u]) =>
+ (Const (@{const_name "op ="}, Type (_, [Type ("fun", _), _])), _) => NONE
+ | (Const (@{const_name "op ="}, _), [t, u]) =>
let
val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
@@ -1731,7 +1734,7 @@
SOME (Codegen.parens
(Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
end
- | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
+ | (t as Const (@{const_name "op ="}, _), ts) => SOME (Codegen.invoke_codegen
thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
| _ => NONE);
@@ -2050,7 +2053,7 @@
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
local
- fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
+ fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
| wrong_prem (Bound _) = true
| wrong_prem _ = false;
val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);