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_set.ML
changeset 32035 8e77b6a250d5
parent 31998 2c7a24f74db9
child 32135 f645b51e8e54 
--- a/src/HOL/Tools/inductive_set.ML	Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Fri Jul 17 23:11:40 2009 +0200
@@ -324,7 +324,7 @@
 fun to_pred_proc thy rules t = case lookup_rule thy I rules t of
     NONE => NONE
   | SOME (lhs, rhs) =>
-      SOME (Envir.subst_vars
+      SOME (Envir.subst_term
         (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rhs);
 
 fun to_pred thms ctxt thm =
isabelle