src/Provers/classical.ML
changeset 15531 08c8dad8e399
parent 15452 e2a721567f67
child 15570 8d8c70b41bab
     1.1 --- a/src/Provers/classical.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Provers/classical.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -224,7 +224,7 @@
     1.4    (case try (fn () =>
     1.5      rule_by_tactic (TRYALL (etac revcut_rl))
     1.6        (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd)) () of
     1.7 -    Some th' => th'
     1.8 +    SOME th' => th'
     1.9    | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th));
    1.10  
    1.11