# HG changeset patch
# User wenzelm
# Date 1236869698 -3600
# Node ID e0b66c11e7e4ef70655568f06504ddc91f9daa78
# Parent  9dea0866021c630674d0c70acb385b2f1a3d5255
Assumption.all_prems_of, Assumption.all_assms_of;

diff -r 9dea0866021c -r e0b66c11e7e4 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu Mar 12 15:54:19 2009 +0100
+++ b/src/HOL/Import/shuffler.ML	Thu Mar 12 15:54:58 2009 +0100
@@ -662,7 +662,7 @@
 fun search_meth ctxt =
     let
         val thy = ProofContext.theory_of ctxt
-        val prems = Assumption.prems_of ctxt
+        val prems = Assumption.all_prems_of ctxt
     in
         Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
     end
diff -r 9dea0866021c -r e0b66c11e7e4 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Mar 12 15:54:19 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Thu Mar 12 15:54:58 2009 +0100
@@ -419,7 +419,7 @@
         val expr = ([(suffix valuetypesN name, 
                      (("",false),Expression.Positional (map SOME pars)))],[]);
       in
-        prove_interpretation_in (ALLGOALS o solve_tac o Assumption.prems_of)
+        prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of)
           (suffix valuetypesN name, expr) thy
       end;
 
diff -r 9dea0866021c -r e0b66c11e7e4 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Mar 12 15:54:19 2009 +0100
+++ b/src/Pure/Isar/args.ML	Thu Mar 12 15:54:58 2009 +0100
@@ -227,7 +227,7 @@
 val bang_facts = Scan.peek (fn context =>
   P.position ($$$ "!") >> (fn (_, pos) =>
     (warning ("use of prems in proof method" ^ Position.str_of pos);
-      Assumption.prems_of (Context.proof_of context))) || Scan.succeed []);
+      Assumption.all_prems_of (Context.proof_of context))) || Scan.succeed []);
 
 val from_to =
   P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
diff -r 9dea0866021c -r e0b66c11e7e4 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Mar 12 15:54:19 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Thu Mar 12 15:54:58 2009 +0100
@@ -135,7 +135,7 @@
 fun export inner outer =    (*beware of closure sizes*)
   let
     val exp = Assumption.export false inner outer;
-    val prems = Assumption.prems_of inner;
+    val prems = Assumption.all_prems_of inner;
   in fn th =>
     let
       val th' = exp th;
diff -r 9dea0866021c -r e0b66c11e7e4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 12 15:54:19 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 12 15:54:58 2009 +0100
@@ -301,7 +301,7 @@
   in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
 
 fun pretty_thm ctxt th =
-  let val asms = map Thm.term_of (Assumption.assms_of ctxt)
+  let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
   in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
 
 fun pretty_thms ctxt [th] = pretty_thm ctxt th
@@ -1370,7 +1370,7 @@
           Pretty.commas (map prt_fix fixes))];
 
       (*prems*)
-      val prems = Assumption.prems_of ctxt;
+      val prems = Assumption.all_prems_of ctxt;
       val len = length prems;
       val suppressed = len - ! prems_limit;
       val prt_prems = if null prems then []
diff -r 9dea0866021c -r e0b66c11e7e4 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Mar 12 15:54:19 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Mar 12 15:54:58 2009 +0100
@@ -52,7 +52,7 @@
     val fixes =
       map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
     val assumes =
-      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.assms_of ctxt);
+      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.all_assms_of ctxt);
     val elems =
       (if null fixes then [] else [Element.Fixes fixes]) @
       (if null assumes then [] else [Element.Assumes assumes]);
@@ -109,7 +109,7 @@
     val th = Goal.norm_result raw_th;
     val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
     val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
-    val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
+    val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt);
     val nprems = Thm.nprems_of th' - Thm.nprems_of th;
 
     (*export fixes*)
diff -r 9dea0866021c -r e0b66c11e7e4 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Mar 12 15:54:19 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Thu Mar 12 15:54:58 2009 +0100
@@ -336,7 +336,7 @@
 
 fun find_theorems ctxt opt_goal rem_dups raw_criteria =
   let
-    val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.prems_of ctxt) 1));
+    val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.all_prems_of ctxt) 1));
     val opt_goal' = Option.map add_prems opt_goal;
 
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
diff -r 9dea0866021c -r e0b66c11e7e4 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Mar 12 15:54:19 2009 +0100
+++ b/src/Pure/goal.ML	Thu Mar 12 15:54:58 2009 +0100
@@ -110,7 +110,7 @@
     val cert = Thm.cterm_of thy;
     val certT = Thm.ctyp_of thy;
 
-    val assms = Assumption.assms_of ctxt;
+    val assms = Assumption.all_assms_of ctxt;
     val As = map Thm.term_of assms;
 
     val xs = map Free (fold Term.add_frees (prop :: As) []);
diff -r 9dea0866021c -r e0b66c11e7e4 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Mar 12 15:54:19 2009 +0100
+++ b/src/Tools/quickcheck.ML	Thu Mar 12 15:54:58 2009 +0100
@@ -144,7 +144,7 @@
 fun test_goal_auto int state =
   let
     val ctxt = Proof.context_of state;
-    val assms = map term_of (Assumption.assms_of ctxt);
+    val assms = map term_of (Assumption.all_assms_of ctxt);
     val Test_Params { size, iterations, default_type } =
       (snd o Data.get o Proof.theory_of) state;
     fun test () =