# HG changeset patch # User wenzelm # Date 809953735 -7200 # Node ID 45ac644b005260b0bae8385cbc5de1f23a34c343 # Parent b54d51df90657f3984d660f28f7661ef42f7e196 adapted to new version of shyps-stuff; diff -r b54d51df9065 -r 45ac644b0052 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Wed Aug 30 14:04:39 1995 +0200 +++ b/src/Pure/axclass.ML Fri Sep 01 13:08:55 1995 +0200 @@ -121,11 +121,11 @@ let fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]); - val {sign, shyps, hyps, prop, ...} = rep_thm thm; + val {sign, hyps, prop, ...} = rep_thm thm; in if not (Sign.subsig (sign, sign_of thy)) then err "theorem not of same theory" - else if not (null shyps) orelse not (null hyps) then + else if not (null (extra_shyps thm)) orelse not (null hyps) then err "theorem may not contain hypotheses" else prop end; diff -r b54d51df9065 -r 45ac644b0052 src/Pure/drule.ML --- a/src/Pure/drule.ML Wed Aug 30 14:04:39 1995 +0200 +++ b/src/Pure/drule.ML Fri Sep 01 13:08:55 1995 +0200 @@ -109,7 +109,7 @@ fun ancestry_of thy = thy :: flat (map ancestry_of (parents_of thy)); -val all_axioms_of = +val all_axioms_of = flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of; @@ -293,13 +293,14 @@ fun pretty_thm th = let - val {sign, shyps, hyps, prop, ...} = rep_thm th; - val hlen = length shyps + length hyps; + val {sign, hyps, prop, ...} = rep_thm th; + val xshyps = extra_shyps th; + val hlen = length xshyps + length hyps; val hsymbs = if hlen = 0 then [] else if ! show_hyps then [Pretty.brk 2, Pretty.list "[" "]" - (map (Sign.pretty_term sign) hyps @ map Sign.pretty_sort shyps)] + (map (Sign.pretty_term sign) hyps @ map Sign.pretty_sort xshyps)] else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")]; in @@ -537,7 +538,7 @@ all generality expressed by Vars having index 0.*) fun standard th = let val {maxidx,...} = rep_thm th - in + in th |> implies_intr_hyps |> strip_shyps |> implies_intr_shyps |> forall_intr_frees |> forall_elim_vars (maxidx + 1) @@ -670,7 +671,7 @@ val vars = distinct (term_vars' prop); in forall_intr_list (map (cterm_of sign) vars) th end; -fun weak_eq_thm (tha,thb) = +fun weak_eq_thm (tha,thb) = eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));