# HG changeset patch # User wenzelm # Date 1119025994 -7200 # Node ID e871f4b1a4f0357916420fa6dcc00024f3f6abce # Parent d2203a276b0791d90be79f5a4f98ae50c9ad3ca7 replaced obsolete theory_of_sign by theory_of_thm; diff -r d2203a276b07 -r e871f4b1a4f0 src/HOL/Modelcheck/MuckeSyn.ML --- 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; diff -r d2203a276b07 -r e871f4b1a4f0 src/HOL/Modelcheck/mucke_oracle.ML --- 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)))