# HG changeset patch
# User wenzelm
# Date 1467620996 -7200
# Node ID e9e677b730111c487a9051741026569cc8a42b60
# Parent  6c731c8b7f0324fcadd82cd71f5a112f0e9e48f8
tuned signature;

diff -r 6c731c8b7f03 -r e9e677b73011 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sat Jul 02 20:22:25 2016 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon Jul 04 10:29:56 2016 +0200
@@ -61,7 +61,7 @@
 fun put_calculation calc =
   `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
      (Data.map (apsnd (K (Option.map (rpair lev) calc))))))
-  #> Proof.put_thms false (calculationN, calc);
+  #> Proof.map_context (Proof_Context.put_thms false (calculationN, calc));
 
 
 
diff -r 6c731c8b7f03 -r e9e677b73011 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Jul 02 20:22:25 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jul 04 10:29:56 2016 +0200
@@ -19,7 +19,6 @@
   val map_context_result : (context -> 'a * context) -> state -> 'a * state
   val map_contexts: (context -> context) -> state -> state
   val propagate_ml_env: state -> state
-  val put_thms: bool -> string * thm list option -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
   val set_facts: thm list -> state -> state
@@ -241,8 +240,6 @@
 fun propagate_ml_env state = map_contexts
   (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
 
-val put_thms = map_context oo Proof_Context.put_thms;
-
 
 (* facts *)
 
@@ -260,7 +257,7 @@
 
 fun put_facts facts =
   map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
-  put_thms true (Auto_Bind.thisN, facts);
+  map_context (Proof_Context.put_thms true (Auto_Bind.thisN, facts));
 
 val set_facts = put_facts o SOME;
 val reset_facts = put_facts NONE;