src/HOL/Nominal/nominal_fresh_fun.ML
changeset 33040 cffdb7b28498
parent 33034 66ef64a5f122
child 34885 6587c24ef6d8
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Oct 21 08:16:25 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Oct 21 10:15:31 2009 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4      fun inst_fresh vars params i st =
     1.5     let val vars' = OldTerm.term_vars (prop_of st);
     1.6         val thy = theory_of_thm st;
     1.7 -   in case vars' \\ vars of
     1.8 +   in case subtract (op =) vars vars' of
     1.9       [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
    1.10      | _ => error "fresh_fun_simp: Too many variables, please report."
    1.11    end