src/Pure/Isar/local_defs.ML
changeset 30473 e0b66c11e7e4
parent 30434 9b94b1358b95
child 30585 6b2ba4666336
     1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Mar 12 15:54:19 2009 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Mar 12 15:54:58 2009 +0100
     1.3 @@ -135,7 +135,7 @@
     1.4  fun export inner outer =    (*beware of closure sizes*)
     1.5    let
     1.6      val exp = Assumption.export false inner outer;
     1.7 -    val prems = Assumption.prems_of inner;
     1.8 +    val prems = Assumption.all_prems_of inner;
     1.9    in fn th =>
    1.10      let
    1.11        val th' = exp th;