1.1 --- a/src/HOL/Library/Multiset.thy Thu May 27 15:28:23 2010 +0200
1.2 +++ b/src/HOL/Library/Multiset.thy Thu May 27 16:42:03 2010 +0200
1.3 @@ -1699,7 +1699,6 @@
1.4 by (fact multiset_order.less_asym)
1.5
1.6 ML {*
1.7 -(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *)
1.8 fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T]))
1.9 (Const _ $ t') =
1.10 let
1.11 @@ -1727,4 +1726,4 @@
1.12 Nitpick.register_term_postprocessor @{typ "'a multiset"} multiset_postproc
1.13 *}
1.14
1.15 -end
1.16 \ No newline at end of file
1.17 +end