src/Pure/Isar/expression.ML
changeset 45589 bb944d58ac19
parent 45588 5eb47a1e4ca7
child 46856 28909eecdf5b
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Nov 19 15:34:37 2011 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Nov 19 16:16:33 2011 +0100
     1.3 @@ -895,7 +895,7 @@
     1.4        |> fst;  (* FIXME duplication to add_thmss *)
     1.5    in
     1.6      ctxt
     1.7 -    |> Locale.add_thmss target Thm.lemmaK facts
     1.8 +    |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts)
     1.9      |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
    1.10        fn thy =>
    1.11          Locale.add_dependency target