# 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;