--- 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
--- 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;
--- 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) ||
--- 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;
--- 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 []
--- 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*)
--- 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;
--- 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) []);
--- 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 () =