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/Predicate_Compile/predicate_compile.ML
changeset 33671 4b0f2599ed48
parent 33630 68e058d061f5
child 33752 9aa8e961f850 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 13 20:41:29 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 13 21:11:15 2009 +0100
@@ -137,8 +137,8 @@
   in
     if (is_inductify options) then
       let
-        val lthy' = LocalTheory.theory (preprocess options const) lthy
-          |> LocalTheory.checkpoint
+        val lthy' = Local_Theory.theory (preprocess options const) lthy
+          |> Local_Theory.checkpoint
         val const =
           case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
             SOME c => c
isabelle