Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/res_axioms.ML
changeset 16925 0fd7b1438d28
parent 16897 7e5319d0f418
child 17261 193b84a70ca4 
--- a/src/HOL/Tools/res_axioms.ML	Wed Jul 27 11:28:18 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Wed Jul 27 11:30:34 2005 +0200
@@ -381,6 +381,7 @@
     let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
         val isa_clauses' = rm_Eps [] isa_clauses
         val clauses_n = length isa_clauses
+        val thy = theory_of_thm thm
 	fun make_axiom_clauses _ [] []= []
 	  | make_axiom_clauses i (cls::clss) (cls'::clss') =
 	      (ResClause.make_axiom_clause cls (thm_name,i), cls') ::
isabelle