1.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4            |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
     1.5          val less_def' = Syntax.check_term lthy3 less_def;
     1.6          val ((_, (_, less_definition')), lthy4) = lthy3
     1.7 -          |> Specification.definition (NONE, (("less_" ^ name ^ "_def", []), less_def'));
     1.8 +          |> Specification.definition (NONE, ((Name.binding ("less_" ^ name ^ "_def"), []), less_def'));
     1.9          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
    1.10          val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
    1.11          val thy5 = lthy4