1.1 --- a/src/Pure/Isar/specification.ML	Tue Nov 14 15:29:50 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Tue Nov 14 15:29:52 2006 +0100
     1.3 @@ -283,8 +283,7 @@
     1.4        end;
     1.5    in
     1.6      goal_ctxt
     1.7 -    |> Proof.global_goal (K (K ())) Attrib.attribute_i ProofContext.bind_propp_schematic_i
     1.8 -      kind before_qed after_qed' NONE (name, []) stmt
     1.9 +    |> Proof.theorem_i kind before_qed after_qed' (map snd stmt)
    1.10      |> Proof.refine_insert facts
    1.11    end;
    1.12