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/inductive_codegen.ML
changeset 32957 675c0c7e6a37
parent 32952 aeb1e44fbc19
child 33037 b22e44496dc2 
--- a/src/HOL/Tools/inductive_codegen.ML	Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Sat Oct 17 00:52:37 2009 +0200
@@ -477,7 +477,7 @@
       (fn NONE => "X" | SOME k' => string_of_int k')
         (ks @ [SOME k]))) arities));
 
-fun prep_intrs intrs = map (rename_term o #prop o rep_thm o standard) intrs;
+fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.standard) intrs;
 
 fun constrain cs [] = []
   | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of
isabelle