adapted to new version of shyps-stuff;
authorwenzelm
Fri Sep 01 13:08:55 1995 +0200 (1995-09-01)
changeset 123745ac644b0052
parent 1236 b54d51df9065
child 1238 289c573327f0
adapted to new version of shyps-stuff;
src/Pure/axclass.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/axclass.ML	Wed Aug 30 14:04:39 1995 +0200
     1.2 +++ b/src/Pure/axclass.ML	Fri Sep 01 13:08:55 1995 +0200
     1.3 @@ -121,11 +121,11 @@
     1.4    let
     1.5      fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]);
     1.6  
     1.7 -    val {sign, shyps, hyps, prop, ...} = rep_thm thm;
     1.8 +    val {sign, hyps, prop, ...} = rep_thm thm;
     1.9    in
    1.10      if not (Sign.subsig (sign, sign_of thy)) then
    1.11        err "theorem not of same theory"
    1.12 -    else if not (null shyps) orelse not (null hyps) then
    1.13 +    else if not (null (extra_shyps thm)) orelse not (null hyps) then
    1.14        err "theorem may not contain hypotheses"
    1.15      else prop
    1.16    end;
     2.1 --- a/src/Pure/drule.ML	Wed Aug 30 14:04:39 1995 +0200
     2.2 +++ b/src/Pure/drule.ML	Fri Sep 01 13:08:55 1995 +0200
     2.3 @@ -109,7 +109,7 @@
     2.4  fun ancestry_of thy =
     2.5    thy :: flat (map ancestry_of (parents_of thy));
     2.6  
     2.7 -val all_axioms_of = 
     2.8 +val all_axioms_of =
     2.9    flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
    2.10  
    2.11  
    2.12 @@ -293,13 +293,14 @@
    2.13  
    2.14  fun pretty_thm th =
    2.15    let
    2.16 -    val {sign, shyps, hyps, prop, ...} = rep_thm th;
    2.17 -    val hlen = length shyps + length hyps;
    2.18 +    val {sign, hyps, prop, ...} = rep_thm th;
    2.19 +    val xshyps = extra_shyps th;
    2.20 +    val hlen = length xshyps + length hyps;
    2.21      val hsymbs =
    2.22        if hlen = 0 then []
    2.23        else if ! show_hyps then
    2.24          [Pretty.brk 2, Pretty.list "[" "]"
    2.25 -          (map (Sign.pretty_term sign) hyps @ map Sign.pretty_sort shyps)]
    2.26 +          (map (Sign.pretty_term sign) hyps @ map Sign.pretty_sort xshyps)]
    2.27        else
    2.28          [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")];
    2.29    in
    2.30 @@ -537,7 +538,7 @@
    2.31      all generality expressed by Vars having index 0.*)
    2.32  fun standard th =
    2.33    let val {maxidx,...} = rep_thm th
    2.34 -  in  
    2.35 +  in
    2.36      th |> implies_intr_hyps
    2.37      |> strip_shyps |> implies_intr_shyps
    2.38      |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
    2.39 @@ -670,7 +671,7 @@
    2.40        val vars = distinct (term_vars' prop);
    2.41    in forall_intr_list (map (cterm_of sign) vars) th end;
    2.42  
    2.43 -fun weak_eq_thm (tha,thb) = 
    2.44 +fun weak_eq_thm (tha,thb) =
    2.45      eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));
    2.46  
    2.47