Proof.put_thms_internal;
authorwenzelm
Thu, 16 Feb 2006 18:25:58 +0100
changeset 19074 77580f732e37
parent 19073 fce515f7759c
child 19075 12833c7e0fa6
Proof.put_thms_internal;
src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Feb 16 18:25:56 2006 +0100
+++ b/src/Pure/Isar/calculation.ML	Thu Feb 16 18:25:58 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 (calculationN, calc);
+  #> Proof.put_thms_internal (calculationN, calc);