changeset 54386 | 3514fdfdf59b |
parent 54285 | 578371ba74cc |
--- a/src/HOL/BNF/Tools/ctr_sugar.ML Mon Nov 11 18:37:56 2013 +0100 +++ b/src/HOL/BNF/Tools/ctr_sugar.ML Mon Nov 11 20:51:00 2013 +0100 @@ -297,7 +297,7 @@ fun qualify mandatory = Binding.qualify mandatory fc_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix); - fun dest_TFree_or_TVar (TFree p) = p + fun dest_TFree_or_TVar (TFree sS) = sS | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S) | dest_TFree_or_TVar _ = error "Invalid type argument";