src/Pure/Isar/calculation.ML
changeset 14549 ea6e18e5c7a9
parent 14282 b23f028c1651
child 14555 341908d6c792
     1.1 --- a/src/Pure/Isar/calculation.ML	Tue Apr 13 07:45:07 2004 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Tue Apr 13 07:47:31 2004 +0200
     1.3 @@ -139,9 +139,13 @@
     1.4  val calculationN = "calculation";
     1.5  
     1.6  fun maintain_calculation false calc state =
     1.7 +    let val facts = Proof.the_facts state 
     1.8 +    in
     1.9        state
    1.10        |> put_calculation calc
    1.11        |> Proof.simple_have_thms calculationN calc
    1.12 +      |> Proof.simple_have_thms Proof.thisN facts
    1.13 +    end
    1.14    | maintain_calculation true calc state =
    1.15        state
    1.16        |> reset_calculation