src/Pure/assumption.ML

 (*  Title:      Pure/assumption.ML
     Author:     Makarius
 
-Local assumptions, parameterized by export rules.
+Context assumptions, parameterized by export rules.
 *)
 
 signature ASSUMPTION =
 sig
   type export
   val assume_export: export
   val presume_export: export
   val assume: cterm -> thm
-  val assms_of: Proof.context -> cterm list
-  val prems_of: Proof.context -> thm list
+  val all_assms_of: Proof.context -> cterm list
+  val all_prems_of: Proof.context -> thm list
   val extra_hyps: Proof.context -> thm -> term list
+  val local_assms_of: Proof.context -> Proof.context -> cterm list
+  val local_prems_of: Proof.context -> Proof.context -> thm list
   val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
   val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
-  val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context
   val export: bool -> Proof.context -> Proof.context -> thm -> thm
   val export_term: Proof.context -> Proof.context -> term -> term
   val export_morphism: Proof.context -> Proof.context -> morphism
 end;
 

 );
 
 fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
 fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
 
-val assumptions_of = #assms o rep_data;
-val assms_of = maps #2 o assumptions_of;
-val prems_of = #prems o rep_data;
 
-fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th);
+(* all assumptions *)
+
+val all_assumptions_of = #assms o rep_data;
+val all_assms_of = maps #2 o all_assumptions_of;
+val all_prems_of = #prems o rep_data;
+
+fun extra_hyps ctxt th =
+  subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
+
+(*named prems -- legacy feature*)
+val _ = Context.>>
+  (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
+    fn Context.Theory _ => [] | Context.Proof ctxt => all_prems_of ctxt)));
 
 
-(* named prems -- legacy feature *)
+(* local assumptions *)
 
-val _ = Context.>>
-  (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
-    fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
+fun local_assumptions_of inner outer =
+  Library.drop (length (all_assumptions_of outer), all_assumptions_of inner);
+
+val local_assms_of = maps #2 oo local_assumptions_of;
+
+fun local_prems_of inner outer =
+  Library.drop (length (all_prems_of outer), all_prems_of inner);
 
 
 (* add assumptions *)
 
 fun add_assms export new_asms =

     pair new_prems
   end;
 
 val add_assumes = add_assms assume_export;
 
-fun add_view outer view = map_data (fn (asms, prems) =>
-  let
-    val (asms1, asms2) = chop (length (assumptions_of outer)) asms;
-    val asms' = asms1 @ [(assume_export, view)] @ asms2;
-  in (asms', prems) end);
-
 
 (* export *)
 
-fun diff_assms inner outer =
-  Library.drop (length (assumptions_of outer), assumptions_of inner);
-
 fun export is_goal inner outer =
-  let val asms = diff_assms inner outer in
+  let val asms = local_assumptions_of inner outer in
     MetaSimplifier.norm_hhf_protect
     #> fold_rev (fn (e, As) => #1 (e is_goal As)) asms
     #> MetaSimplifier.norm_hhf_protect
   end;
 
 fun export_term inner outer =
-  fold_rev (fn (e, As) => #2 (e false As)) (diff_assms inner outer);
+  fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
 
 fun export_morphism inner outer =
   let
     val thm = export false inner outer;
     val term = export_term inner outer;