# HG changeset patch
# User wenzelm
# Date 1153867487 -7200
# Node ID 974d98969ba695d4e822dcb5d9531c0ab9025240
# Parent  90e551baac6ad4738d28bb4a7dd6263e0a3e08a7
moved pprint functions to Isar/proof_display.ML;
added primitive add_assumes;
tuned internal prems: no names;

diff -r 90e551baac6a -r 974d98969ba6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jul 26 00:44:46 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jul 26 00:44:47 2006 +0200
@@ -127,14 +127,15 @@
   val fix_frees: term -> context -> context
   val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a)
   val bind_fixes: string list -> context -> (term -> term) * context
+  val assume_export: export
+  val presume_export: export
+  val add_assumes: cterm list -> context -> thm list * context
   val add_assms: export ->
     ((string * attribute list) * (string * string list) list) list ->
     context -> (bstring * thm list) list * context
   val add_assms_i: export ->
     ((string * attribute list) * (term * term list) list) list ->
     context -> (bstring * thm list) list * context
-  val assume_export: export
-  val presume_export: export
   val add_view: context -> cterm list -> context -> context
   val export_view: cterm list -> context -> context -> thm -> thm
   val add_cases: bool -> (string * RuleCases.T option) list -> context -> context
@@ -152,8 +153,6 @@
   val prems_limit: int ref
   val pretty_ctxt: context -> Pretty.T list
   val pretty_context: context -> Pretty.T list
-  val debug: bool ref
-  val pprint_context: context -> pprint_args -> unit
 end;
 
 structure ProofContext: PROOF_CONTEXT =
@@ -179,7 +178,7 @@
     consts: Consts.T * Consts.T,                  (*global/local consts*)
     assms:
       ((cterm list * export) list *               (*assumes and views: A ==> _*)
-        (string * thm list) list),                (*prems: A |- A*)
+        thm list),                                (*prems: A |- A*)
     thms: thm list NameSpace.table * FactIndex.T, (*local thms*)
     cases: (string * (RuleCases.T * bool)) list}; (*local contexts*)
 
@@ -244,7 +243,7 @@
 
 val assumptions_of = #1 o #assms o rep_context;
 val assms_of = map Thm.term_of o maps #1 o assumptions_of;
-val prems_of = maps #2 o #2 o #assms o rep_context;
+val prems_of = #2 o #assms o rep_context;
 
 val thms_of = #thms o rep_context;
 val fact_index_of = #2 o thms_of;
@@ -960,44 +959,7 @@
 
 (** assumptions **)
 
-(* generic assms *)
-
-local
-
-fun gen_assm ((name, attrs), props) ctxt =
-  let
-    val cprops = map (Thm.cterm_of (theory_of ctxt)) props;
-    val asms = map (Goal.norm_hhf o Thm.assume) cprops;
-
-    val ths = map (fn th => ([th], [])) asms;
-    val ([(_, thms)], ctxt') =
-      ctxt
-      |> auto_bind_facts props
-      |> note_thmss_i [((name, attrs), ths)];
-  in ((cprops, (name, asms), (name, thms)), ctxt') end;
-
-fun gen_assms prepp exp args ctxt =
-  let
-    val (propss, ctxt1) = swap (prepp (ctxt, map snd args));
-    val (results, ctxt2) = fold_map gen_assm (map fst args ~~ propss) ctxt1;
-
-    val new_asms = maps #1 results;
-    val new_prems = map #2 results;
-    val ctxt3 = ctxt2
-      |> map_assms (fn (asms, prems) => (asms @ [(new_asms, exp)], prems @ new_prems))
-    val ctxt4 = ctxt3
-      |> put_thms_internal (AutoBind.premsN, SOME (prems_of ctxt3));
-  in (map #3 results, tap (Variable.warn_extra_tfrees ctxt) ctxt4) end;
-
-in
-
-val add_assms = gen_assms (apsnd #1 o bind_propp);
-val add_assms_i = gen_assms (apsnd #1 o bind_propp_i);
-
-end;
-
-
-(* basic assumptions *)
+(* basic exports *)
 
 (*
     [A]
@@ -1019,6 +981,46 @@
 fun presume_export _ = assume_export false;
 
 
+(* plain assumptions *)
+
+fun new_prems new_asms new_prems =
+  map_assms (fn (asms, prems) => (asms @ [new_asms], prems @ new_prems)) #>
+  (fn ctxt => put_thms_internal (AutoBind.premsN, SOME (prems_of ctxt)) ctxt);
+
+fun add_assumes asms =
+  let val prems = map (Goal.norm_hhf o Thm.assume) asms
+  in new_prems (asms, assume_export) prems #> pair prems end;
+
+
+(* generic assms *)
+
+local
+
+fun gen_assm ((name, attrs), props) ctxt =
+  let
+    val cprops = map (Thm.cterm_of (theory_of ctxt)) props;
+    val prems = map (Goal.norm_hhf o Thm.assume) cprops;
+    val ([(_, thms)], ctxt') =
+      ctxt
+      |> auto_bind_facts props
+      |> note_thmss_i [((name, attrs), map (fn th => ([th], [])) prems)];
+  in ((cprops, prems, (name, thms)), ctxt') end;
+
+fun gen_assms prepp exp args ctxt =
+  let
+    val (propss, ctxt1) = swap (prepp (ctxt, map snd args));
+    val (results, ctxt2) = fold_map gen_assm (map fst args ~~ propss) ctxt1;
+    val ctxt3 = new_prems (maps #1 results, exp) (maps #2 results) ctxt2;
+  in (map #3 results, tap (Variable.warn_extra_tfrees ctxt) ctxt3) end;
+
+in
+
+val add_assms = gen_assms (apsnd #1 o bind_propp);
+val add_assms_i = gen_assms (apsnd #1 o bind_propp_i);
+
+end;
+
+
 (* additional views *)
 
 fun add_view outer view = map_assms (fn (asms, prems) =>
@@ -1259,13 +1261,4 @@
     verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
   end;
 
-
-(* toplevel pretty printing *)
-
-val debug = ref false;
-
-fun pprint_context ctxt = Pretty.pprint
- (if ! debug then Pretty.quote (Pretty.big_list "proof context:" (pretty_context ctxt))
-  else Pretty.str "<context>");
-
 end;