src/Pure/Isar/obtain.ML
changeset 19300 7689f81f8996
parent 18907 f984f22f1cb4
child 19482 9f11af8f7ef9
     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Mar 21 12:18:06 2006 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Mar 21 12:18:07 2006 +0100
     1.3 @@ -208,7 +208,7 @@
     1.4      val rule' = rule |> Thm.instantiate (instT, []);
     1.5  
     1.6      val tvars = Drule.tvars_of rule';
     1.7 -    val vars = fold (remove op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule');
     1.8 +    val vars = subtract (op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule');
     1.9      val _ =
    1.10        if null tvars andalso null vars then ()
    1.11        else err ("Illegal schematic variable(s) " ^