src/Pure/Isar/code.ML
changeset 28971 300ec36a19af
parent 28708 a1a436f09ec6
child 29302 eb782d1dc07c
     1.1 --- a/src/Pure/Isar/code.ML	Tue Dec 02 14:29:12 2008 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Dec 04 23:00:21 2008 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    val add_default_eqn_attrib: Attrib.src
     1.5    val del_eqn: thm -> theory -> theory
     1.6    val del_eqns: string -> theory -> theory
     1.7 -  val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory
     1.8 +  val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
     1.9    val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    1.10    val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    1.11    val add_inline: thm -> theory -> theory
    1.12 @@ -114,7 +114,7 @@
    1.13  
    1.14  (* defining equations *)
    1.15  
    1.16 -type eqns = bool * (thm * bool) list Lazy.T;
    1.17 +type eqns = bool * (thm * bool) list lazy;
    1.18    (*default flag, theorems with linear flag (perhaps lazy)*)
    1.19  
    1.20  fun pretty_lthms ctxt r = case Lazy.peek r