| changeset 21445 | 0d562bf8ac3e |
| parent 20898 | 113c9516a2d7 |
| child 21506 | b2a673894ce5 |
--- 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);