# 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));