src/Pure/drule.ML
changeset 14387 e96d5c42c4b0
parent 14340 bc93ffa674cc
child 14391 bb726050650d
     1.1 --- a/src/Pure/drule.ML	Sat Feb 14 02:06:12 2004 +0100
     1.2 +++ b/src/Pure/drule.ML	Sun Feb 15 10:46:37 2004 +0100
     1.3 @@ -371,6 +371,12 @@
     1.4  (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
     1.5      all generality expressed by Vars having index 0.*)
     1.6  
     1.7 +fun flexflex_unique th =
     1.8 +    case Seq.chop (2, flexflex_rule th) of
     1.9 +      ([th],_) => th
    1.10 +    | ([],_)   => raise THM("flexflex_unique: impossible constraints", 0, [th])
    1.11 +    |      _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
    1.12 +
    1.13  fun close_derivation thm =
    1.14    if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm)
    1.15    else thm;
    1.16 @@ -378,7 +384,7 @@
    1.17  fun standard' th =
    1.18    let val {maxidx,...} = rep_thm th in
    1.19      th
    1.20 -    |> implies_intr_hyps
    1.21 +    |> flexflex_unique |> implies_intr_hyps 
    1.22      |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
    1.23      |> strip_shyps_warning
    1.24      |> zero_var_indexes |> Thm.varifyT |> Thm.compress