Nominal/nominal_dt_alpha.ML
changeset 2477 2f289c1f6cf1
parent 2476 8f8652a8107f
child 2480 ac7dff1194e8
--- a/Nominal/nominal_dt_alpha.ML	Sat Sep 11 05:56:49 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Sun Sep 12 22:46:40 2010 +0800
@@ -371,7 +371,8 @@
     val true_trms = replicate (length alphas) (K @{term True})
   
     fun apply_all x fs = map (fn f => f x) fs
-      val goals_rhs = 
+    
+    val goals_rhs = 
         group (props @ (alphas ~~ true_trms))
         |> map snd 
         |> map2 apply_all (args1 ~~ args2)