src/HOL/BNF/Tools/ctr_sugar.ML
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";