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/ZF/Tools/inductive_package.ML
changeset 43333 2bdec7f430d3
parent 43324 2b47822868e4
child 43596 78211f66cf8d 
--- a/src/ZF/Tools/inductive_package.ML	Thu Jun 09 22:25:25 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Jun 09 23:12:02 2011 +0200
@@ -493,7 +493,7 @@
        The name "x.1" comes from the "RS spec" !*)
      val inst =
          case elem_frees of [_] => I
-            | _ => instantiate ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
+            | _ => Drule.instantiate_normalize ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
                                       cterm_of thy1 elem_tuple)]);
 
      (*strip quantifier and the implication*)
isabelle