369 |
369 |
370 |
370 |
371 (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers; |
371 (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers; |
372 all generality expressed by Vars having index 0.*) |
372 all generality expressed by Vars having index 0.*) |
373 |
373 |
|
374 fun flexflex_unique th = |
|
375 case Seq.chop (2, flexflex_rule th) of |
|
376 ([th],_) => th |
|
377 | ([],_) => raise THM("flexflex_unique: impossible constraints", 0, [th]) |
|
378 | _ => raise THM("flexflex_unique: multiple unifiers", 0, [th]); |
|
379 |
374 fun close_derivation thm = |
380 fun close_derivation thm = |
375 if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm) |
381 if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm) |
376 else thm; |
382 else thm; |
377 |
383 |
378 fun standard' th = |
384 fun standard' th = |
379 let val {maxidx,...} = rep_thm th in |
385 let val {maxidx,...} = rep_thm th in |
380 th |
386 th |
381 |> implies_intr_hyps |
387 |> flexflex_unique |> implies_intr_hyps |
382 |> forall_intr_frees |> forall_elim_vars (maxidx + 1) |
388 |> forall_intr_frees |> forall_elim_vars (maxidx + 1) |
383 |> strip_shyps_warning |
389 |> strip_shyps_warning |
384 |> zero_var_indexes |> Thm.varifyT |> Thm.compress |
390 |> zero_var_indexes |> Thm.varifyT |> Thm.compress |
385 end; |
391 end; |
386 |
392 |