author | wenzelm |
Tue, 21 Nov 2006 18:07:44 +0100 | |
changeset 21445 | 0d562bf8ac3e |
parent 21444 | 8f71e2b3fd92 |
child 21446 | 3d57db34633b |
--- 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);