removed extra shyps error;
authorwenzelm
Wed Sep 29 13:49:07 1999 +0200 (1999-09-29)
changeset 763225a0d2ba3a87
parent 7631 1b6b51b17c4a
child 7633 838077e40a46
removed extra shyps error;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Sep 29 13:48:35 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Sep 29 13:49:07 1999 +0200
     1.3 @@ -472,21 +472,10 @@
     1.4  fun strip_flexflex thm =
     1.5    Seq.hd (Thm.flexflex_rule thm) handle THM _ => thm;
     1.6  
     1.7 -fun final_result state pre_thm =
     1.8 -  let
     1.9 -    val thm =
    1.10 -      pre_thm
    1.11 -      |> strip_flexflex
    1.12 -      |> Thm.strip_shyps
    1.13 -      |> Drule.standard;
    1.14 -
    1.15 -    val str_of_sort = Sign.str_of_sort (Thm.sign_of_thm thm);
    1.16 -    val xshyps = Thm.extra_shyps thm;
    1.17 -  in
    1.18 -    if not (null xshyps) then
    1.19 -      raise STATE ("Extra sort hypotheses: " ^ commas (map str_of_sort xshyps), state)
    1.20 -    else thm
    1.21 -  end;
    1.22 +fun final_result state thm =
    1.23 +  thm
    1.24 +  |> strip_flexflex
    1.25 +  |> Drule.standard;
    1.26  
    1.27  
    1.28