Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
LocalTheory -> Local_Theory
authorhuffman
Fri, 13 Nov 2009 16:10:04 -0800
changeset 33681 cddea85bc87b
parent 33680 a47277e09012
child 33682 0c5d1485dea7
child 33692 ac68c3ee4c2e
LocalTheory -> Local_Theory
src/HOLCF/Tools/repdef.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Tools/repdef.ML	Fri Nov 13 15:40:06 2009 -0800
+++ b/src/HOLCF/Tools/repdef.ML	Fri Nov 13 16:10:04 2009 -0800
@@ -126,7 +126,7 @@
     val thy4 = lthy3
       |> Class.prove_instantiation_instance
           (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1))
-      |> LocalTheory.exit_global;
+      |> Local_Theory.exit_global;
 
     (*other theorems*)
     val typedef_thms' = map (Thm.transfer thy4)
isabelle