avoid polymorphic equality;
authorwenzelm
Tue Mar 21 12:18:19 2006 +0100 (2006-03-21)
changeset 19308033160ed1c8b
parent 19307 2beb7153e657
child 19309 8ea43e9ad83a
avoid polymorphic equality;
subtract (op =);
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Mar 21 12:18:18 2006 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Mar 21 12:18:19 2006 +0100
     1.3 @@ -261,11 +261,11 @@
     1.4      else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode")
     1.5    end;
     1.6  
     1.7 -val assert_forward = assert_mode (equal Forward);
     1.8 -val assert_chain = assert_mode (equal Chain);
     1.9 -val assert_forward_or_chain = assert_mode (equal Forward orf equal Chain);
    1.10 -val assert_backward = assert_mode (equal Backward);
    1.11 -val assert_no_chain = assert_mode (not_equal Chain);
    1.12 +val assert_forward = assert_mode (fn mode => mode = Forward);
    1.13 +val assert_chain = assert_mode (fn mode => mode = Chain);
    1.14 +val assert_forward_or_chain = assert_mode (fn mode => mode = Forward orelse mode = Chain);
    1.15 +val assert_backward = assert_mode (fn mode => mode = Backward);
    1.16 +val assert_no_chain = assert_mode (fn mode => mode <> Chain);
    1.17  
    1.18  val enter_forward = put_mode Forward;
    1.19  val enter_chain = put_mode Chain;
    1.20 @@ -488,7 +488,7 @@
    1.21            [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))));
    1.22  
    1.23      val {hyps, thy, ...} = Thm.rep_thm goal;
    1.24 -    val bad_hyps = fold (remove (op aconv)) (ProofContext.assms_of ctxt) hyps;
    1.25 +    val bad_hyps = subtract (op aconv) (ProofContext.assms_of ctxt) hyps;
    1.26      val _ = conditional (not (null bad_hyps)) (fn () => error ("Additional hypotheses:\n" ^
    1.27          cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps)));
    1.28