--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 05 15:53:31 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 05 16:00:53 2012 +0200
@@ -64,10 +64,9 @@
val As' = map dest_TFree As;
val _ = (case duplicates (op =) As of [] => ()
- | T :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy T)));
+ | A :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy A)));
(* TODO: print timing information for sugar *)
- (* TODO: check that no type variables occur in the rhss that's not in the lhss *)
(* TODO: use sort constraints on type args *)
(* TODO: use mixfix *)
@@ -95,6 +94,14 @@
val sel_bindersss = map (map (map fst)) ctr_argsss;
val ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
+ val rhs_As = (case subtract (op =) As' (fold (fold (fold Term.add_tfreesT)) ctr_Tsss []) of
+ [] => ()
+ | A' :: _ => error ("Extra type variables on rhs: " ^
+ quote (Syntax.string_of_typ lthy (TFree A'))));
+
+ (* TODO: check that no type variables occur in the rhss that's not in the lhss *)
+
+
val (Bs, C) =
lthy
|> fold (fold (fn s => Variable.declare_typ (TFree (s, dummyS))) o type_args_of) specs