--- a/src/HOL/Modelcheck/MuckeSyn.ML Fri Jun 17 18:33:13 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML Fri Jun 17 18:33:14 2005 +0200
@@ -132,12 +132,12 @@
fun mk_lam_def (_::_) _ _ = NONE
| mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t
| mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t =
- let val tsig = #sign (rep_thm t);
- val fnam = Sign.string_of_term tsig (getfun LHS);
- val rhs = Sign.string_of_term tsig (freeze_thaw RHS)
+ let val thy = theory_of_thm t;
+ val fnam = Sign.string_of_term thy (getfun LHS);
+ val rhs = Sign.string_of_term thy (freeze_thaw RHS)
val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
in
- SOME (prove_goal (theory_of_sign tsig) gl (fn prems =>
+ SOME (prove_goal thy gl (fn prems =>
[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
end
| mk_lam_def [] _ t= NONE;
--- a/src/HOL/Modelcheck/mucke_oracle.ML Fri Jun 17 18:33:13 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Fri Jun 17 18:33:14 2005 +0200
@@ -984,8 +984,8 @@
val s = post_last_dot(fst(qtn a));
fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t))))) = t |
param_types _ = error "malformed induct-theorem in preprocess_td";
- val pl = param_types (concl_of (get_thm (theory_of_sign sg) (s ^ ".induct", NONE)));
- val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm (theory_of_sign sg) (s ^ ".induct", NONE)));
+ val pl = param_types (concl_of (get_thm sg (s ^ ".induct", NONE)));
+ val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (s ^ ".induct", NONE)));
val ntl = new_types l;
in
((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))