--- a/src/HOL/Nominal/nominal_thmdecls.ML Wed Mar 19 22:27:57 2008 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Wed Mar 19 22:28:08 2008 +0100
@@ -10,6 +10,9 @@
respectively the lemma from the data-slot.
*)
+fun dynamic_thm thy name = PureThy.get_thm thy (Facts.Named (name, NONE));
+fun dynamic_thms thy name = PureThy.get_thms thy (Facts.Named (name, NONE));
+
signature NOMINAL_THMDECLS =
sig
val print_data: Proof.context -> unit
@@ -76,8 +79,6 @@
then (EVERY [tac, print_tac ("after "^msg)])
else tac
-fun dynamic_thms thy name = PureThy.get_thms thy (Name name)
-
fun tactic_eqvt ctx orig_thm pi typi =
let
val mypi = Thm.cterm_of ctx (Var (pi,typi))