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/Library/bnf_axiomatization.ML
changeset 62514 aae510e9a698
parent 62324 ae44f16dcea5
child 62531 b5d656bf0441 
--- a/src/HOL/Library/bnf_axiomatization.ML	Fri Feb 26 22:38:44 2016 +0100
+++ b/src/HOL/Library/bnf_axiomatization.ML	Sat Mar 05 12:49:47 2016 +0100
@@ -83,7 +83,7 @@
 
     val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result
       (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.reset;
 
     fun mk_wit_thms set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
isabelle