# HG changeset patch
# User blanchet
# Date 1459159547 -7200
# Node ID 2b317e347b9b76d59a7122a1ac2709b883b07bc3
# Parent  3d7fe7ec7981297c546f6169692f81131edc2603
more reliable check for rhs variables

diff -r 3d7fe7ec7981 -r 2b317e347b9b src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -786,16 +786,10 @@
       | arg :: _ => error ("Repeated argument: " ^ quote (Syntax.string_of_term ctxt arg)));
 
     fun check_no_other_frees () =
-      let
-        val known_frees = fun_frees @ arg_ts;
-
-        fun check_free (t as Free (s, _)) =
-            Variable.is_fixed ctxt s orelse member (op aconv) known_frees t orelse
-            error ("Unexpected variable: " ^ quote s)
-          | check_free _ = false;
-      in
-        Term.exists_subterm check_free rhs
-      end;
+      (case Term.add_frees rhs [] |> map Free |> subtract (op =) (fun_frees @ arg_ts)
+          |> filter_out (Variable.is_fixed ctxt o fst o dest_Free) of
+        [] => ()
+      | Free (s, _) :: _ => error ("Extra variable on right-hand side: " ^ quote s));
   in
     check_no_duplicate_arg ();
     check_fun_name ();