# HG changeset patch
# User blanchet
# Date 1346853653 -7200
# Node ID c6ccaf6df93c4b77711fe3172ea9bab187ca62a9
# Parent  bd6a18a1a5afe443c5c879989195f25ec52a7120
check type variables on rhs

diff -r bd6a18a1a5af -r c6ccaf6df93c src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- 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