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_specialisation.ML
changeset 45906 0aaeb5520f2f
parent 43324 2b47822868e4
child 50056 72efd6b4038d 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Fri Dec 16 22:07:03 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Sat Dec 17 12:10:37 2011 +0100
@@ -142,7 +142,7 @@
       | restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names =
         replace_term_and_restrict thy T t Tts free_names
       | restrict_pattern' thy ((T as Type (Tcon, Ts), t) :: Tts) free_names =
-        case Datatype_Data.get_constrs thy Tcon of
+        case Datatype.get_constrs thy Tcon of
           NONE => replace_term_and_restrict thy T t Tts free_names
         | SOME constrs => (case strip_comb t of
           (Const (s, _), ats) => (case AList.lookup (op =) constrs s of
isabelle