src/Pure/drule.ML
changeset 11997 402ae1a172ae
parent 11975 129c6679e8c4
child 12005 291593391010
     1.1 --- a/src/Pure/drule.ML	Wed Oct 31 01:28:39 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Oct 31 19:32:05 2001 +0100
     1.3 @@ -661,7 +661,7 @@
     1.4          |> Thm.forall_intr cx
     1.5          |> Thm.implies_intr cphi
     1.6          |> Thm.implies_intr rhs)
     1.7 -    |> store_standard_thm "norm_hhf_eq"
     1.8 +    |> open_store_standard_thm "norm_hhf_eq"
     1.9    end;
    1.10  
    1.11