# HG changeset patch
# User wenzelm
# Date 1155075159 -7200
# Node ID ba1c262c762513a10e8ddbe64a5631860f3530d0
# Parent  867696dc64fc8c823f0d924705423ae52444fdf7
renamed map_theory to theory;
added theory_result;
prems_limit: default ~1;

diff -r 867696dc64fc -r ba1c262c7625 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Aug 09 00:12:38 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Aug 09 00:12:39 2006 +0200
@@ -17,7 +17,8 @@
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
   val fact_index_of: Proof.context -> FactIndex.T
   val transfer: theory -> Proof.context -> Proof.context
-  val map_theory: (theory -> theory) -> Proof.context -> Proof.context
+  val theory: (theory -> theory) -> Proof.context -> Proof.context
+  val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_typ: Proof.context -> typ -> Pretty.T
   val pretty_sort: Proof.context -> sort -> Pretty.T
@@ -230,7 +231,7 @@
 val cases_of = #cases o rep_context;
 
 
-(* transfer *)
+(* theory transfer *)
 
 fun transfer_syntax thy =
   map_syntax (LocalSyntax.rebuild thy) #>
@@ -242,7 +243,11 @@
 
 fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
 
-fun map_theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
+fun theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
+
+fun theory_result f ctxt =
+  let val (res, thy') = f (theory_of ctxt)
+  in (res, ctxt |> transfer thy') end;
 
 
 
@@ -1102,7 +1107,7 @@
 
 (* core context *)
 
-val prems_limit = ref 10;
+val prems_limit = ref ~1;
 
 fun pretty_ctxt ctxt =
   if ! prems_limit < 0 andalso not (! debug) then []
@@ -1128,12 +1133,12 @@
           Pretty.commas (map prt_fix fixes))];
 
       (*prems*)
-      val limit = ! prems_limit;
       val prems = Assumption.prems_of ctxt;
       val len = length prems;
+      val suppressed = len - ! prems_limit;
       val prt_prems = if null prems then []
-        else [Pretty.big_list "prems:" ((if len <= limit then [] else [Pretty.str "..."]) @
-          map (pretty_thm ctxt) (Library.drop (len - limit, prems)))];
+        else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
+          map (pretty_thm ctxt) (Library.drop (suppressed, prems)))];
     in prt_structs @ prt_fixes @ prt_prems end;