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