src/Pure/Isar/expression.ML
changeset 33644 5266a72e0889
parent 33643 b275f26a638b
child 33670 02b7738aef6a
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Nov 12 22:02:11 2009 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Nov 12 22:29:54 2009 +0100
     1.3 @@ -713,7 +713,7 @@
     1.4        fold_map (fn (a, spec) => fn axs =>
     1.5            let val (ps, qs) = chop (length spec) axs
     1.6            in ((a, [(ps, [])]), qs) end) asms axms
     1.7 -      |> apfst (curry Notes Thm.assumptionK)
     1.8 +      |> apfst (curry Notes "")
     1.9    | assumes_to_notes e axms = (e, axms);
    1.10  
    1.11  fun defines_to_notes thy (Defines defs) =