# HG changeset patch # User wenzelm # Date 1164128864 -3600 # Node ID 0d562bf8ac3e72fe846d7656ac663863e1749be1 # Parent 8f71e2b3fd92b531f88ab8212c31d752ed12c813 renamed Proof.put_thms_internal to Proof.put_thms; diff -r 8f71e2b3fd92 -r 0d562bf8ac3e src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Tue Nov 21 18:07:43 2006 +0100 +++ b/src/Pure/Isar/calculation.ML Tue Nov 21 18:07:44 2006 +0100 @@ -62,7 +62,7 @@ fun put_calculation calc = `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map (CalculationData.map (apsnd (K (Option.map (rpair lev) calc)))))) - #> Proof.put_thms_internal (calculationN, calc); + #> Proof.put_thms (calculationN, calc);