| changeset 16767 | 2d4433759b8d |
| parent 16741 | 7a6c17b826c0 |
| child 16794 | 12d00dab5301 |
--- a/src/HOL/Tools/res_clause.ML Mon Jul 11 14:52:55 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Mon Jul 11 16:42:42 2005 +0200 @@ -257,6 +257,7 @@ | fun_name_type _ = raise CLAUSE("Function Not First Order"); +(* FIX - add in funcs and stuff to this *) fun term_of (Var(ind_nm,T)) = let val (folType,ts) = type_of T