src/HOL/Tools/inductive_set.ML
changeset 32035 8e77b6a250d5
parent 31998 2c7a24f74db9
child 32135 f645b51e8e54
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -324,7 +324,7 @@
     1.4  fun to_pred_proc thy rules t = case lookup_rule thy I rules t of
     1.5      NONE => NONE
     1.6    | SOME (lhs, rhs) =>
     1.7 -      SOME (Envir.subst_vars
     1.8 +      SOME (Envir.subst_term
     1.9          (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rhs);
    1.10  
    1.11  fun to_pred thms ctxt thm =