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/Pure/Isar/instance.ML
changeset 25514 4b508bb31a6c
parent 25502 9200b36280c0
child 25536 01753a944433 
--- a/src/Pure/Isar/instance.ML	Fri Nov 30 20:13:07 2007 +0100
+++ b/src/Pure/Isar/instance.ML	Fri Nov 30 20:13:08 2007 +0100
@@ -61,9 +61,9 @@
     |> `(fn ctxt => map (mk_def ctxt) defs)
     |-> (fn defs => fold_map Specification.definition defs)
     |-> (fn defs => `(fn ctxt => export_defs ctxt defs))
-    ||> LocalTheory.exit
-    ||> ProofContext.theory_of
-    ||> TheoryTarget.instantiation arities
+    ||> LocalTheory.reinit
+    (*||> ProofContext.theory_of
+    ||> TheoryTarget.instantiation arities*)
     |-> (fn defs => do_proof defs)
   else
     thy
isabelle