Proof.put_thms_internal;
authorwenzelm
Thu Feb 16 18:25:58 2006 +0100 (2006-02-16)
changeset 1907477580f732e37
parent 19073 fce515f7759c
child 19075 12833c7e0fa6
Proof.put_thms_internal;
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Thu Feb 16 18:25:56 2006 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Thu Feb 16 18:25:58 2006 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4  fun put_calculation calc =
     1.5    `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
     1.6       (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
     1.7 -  #> Proof.put_thms (calculationN, calc);
     1.8 +  #> Proof.put_thms_internal (calculationN, calc);
     1.9  
    1.10  
    1.11