moved basic assumption operations from structure ProofContext to Assumption;

--- a/src/HOL/Import/shuffler.ML	Thu Jul 27 13:43:00 2006 +0200
+++ b/src/HOL/Import/shuffler.ML	Thu Jul 27 13:43:01 2006 +0200
@@ -665,7 +665,7 @@
 fun search_meth ctxt =
     let
 	val thy = ProofContext.theory_of ctxt
-	val prems = ProofContext.prems_of ctxt
+	val prems = Assumption.prems_of ctxt
     in
 	Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy true (map (pair "premise") prems))
     end

--- a/src/HOL/Tools/res_atp.ML	Thu Jul 27 13:43:00 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Jul 27 13:43:01 2006 +0200
@@ -576,7 +576,7 @@
 
 
 fun cnf_hyps_thms ctxt = 
-    let val ths = ProofContext.prems_of ctxt
+    let val ths = Assumption.prems_of ctxt
     in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
 
 

--- a/src/Pure/Isar/args.ML	Thu Jul 27 13:43:00 2006 +0200
+++ b/src/Pure/Isar/args.ML	Thu Jul 27 13:43:01 2006 +0200
@@ -320,7 +320,7 @@
   nat >> PureThy.Single));
 
 val bang_facts = Scan.peek (fn context =>
-  $$$ "!" >> K (ProofContext.prems_of (Context.proof_of context)) || Scan.succeed []);
+  $$$ "!" >> K (Assumption.prems_of (Context.proof_of context)) || Scan.succeed []);
 
 
 (* goal specification *)

--- a/src/Pure/Isar/local_defs.ML	Thu Jul 27 13:43:00 2006 +0200
+++ b/src/Pure/Isar/local_defs.ML	Thu Jul 27 13:43:01 2006 +0200
@@ -10,7 +10,7 @@
   val cert_def: ProofContext.context -> term -> (string * typ) * term
   val abs_def: term -> (string * typ) * term
   val mk_def: ProofContext.context -> (string * term) list -> term list
-  val def_export: ProofContext.export
+  val def_export: Assumption.export
   val add_def: string * term -> ProofContext.context ->
     ((string * typ) * thm) * ProofContext.context
   val print_rules: Context.generic -> unit

--- a/src/Pure/Isar/locale.ML	Thu Jul 27 13:43:00 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Jul 27 13:43:01 2006 +0200
@@ -1816,7 +1816,8 @@
     val pred_ctxt = ProofContext.init pred_thy;
     val (ctxt, (_, facts)) = activate_facts true (K I)
       (pred_ctxt, axiomify predicate_axioms elemss');
-    val export = ProofContext.export_view predicate_statement ctxt thy_ctxt;
+    val export = singleton (ProofContext.export_standard
+        (Assumption.add_view thy_ctxt predicate_statement ctxt) thy_ctxt);
     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
     val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
     val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';

--- a/src/Pure/Isar/method.ML	Thu Jul 27 13:43:00 2006 +0200
+++ b/src/Pure/Isar/method.ML	Thu Jul 27 13:43:01 2006 +0200
@@ -227,7 +227,7 @@
 
 fun assm_tac ctxt =
   assume_tac APPEND'
-  asm_tac (ProofContext.prems_of ctxt) APPEND'
+  asm_tac (Assumption.prems_of ctxt) APPEND'
   cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
   cond_rtac (can Logic.dest_term) Drule.termI;
 

--- a/src/Pure/Isar/obtain.ML	Thu Jul 27 13:43:00 2006 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Jul 27 13:43:01 2006 +0200
@@ -319,7 +319,7 @@
             val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
           in
             ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
-            ctxt' |> ProofContext.add_assms_i ProofContext.assume_export
+            ctxt' |> ProofContext.add_assms_i Assumption.assume_export
               [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
             |>> (fn [(_, [th])] => th)
           end;

--- a/src/Pure/Isar/proof.ML	Thu Jul 27 13:43:00 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jul 27 13:43:01 2006 +0200
@@ -47,9 +47,9 @@
   val let_bind_i: (term list * term) list -> state -> state
   val fix: (string * string option * mixfix) list -> state -> state
   val fix_i: (string * typ option * mixfix) list -> state -> state
-  val assm: ProofContext.export ->
+  val assm: Assumption.export ->
     ((string * Attrib.src list) * (string * string list) list) list -> state -> state
-  val assm_i: ProofContext.export ->
+  val assm_i: Assumption.export ->
     ((string * attribute list) * (term * term list) list) list -> state -> state
   val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
   val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
@@ -476,10 +476,10 @@
     val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
         (pretty_goals_local ctxt "" (true, ! show_main_goal) (! Display.goals_limit) goal @
           [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
-    val _ =
-      (case subtract (op aconv) (ProofContext.assms_of ctxt) (#hyps (Thm.rep_thm goal)) of
-        [] => ()
-      | hyps => error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term hyps)));
+
+    val extra_hyps = Assumption.extra_hyps ctxt goal;
+    val _ = null extra_hyps orelse
+      error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
 
     val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal)
       handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal);
@@ -544,10 +544,10 @@
 
 val assm      = gen_assume ProofContext.add_assms Attrib.attribute;
 val assm_i    = gen_assume ProofContext.add_assms_i (K I);
-val assume    = assm ProofContext.assume_export;
-val assume_i  = assm_i ProofContext.assume_export;
-val presume   = assm ProofContext.presume_export;
-val presume_i = assm_i ProofContext.presume_export;
+val assume    = assm Assumption.assume_export;
+val assume_i  = assm_i Assumption.assume_export;
+val presume   = assm Assumption.presume_export;
+val presume_i = assm_i Assumption.presume_export;
 
 end;