src/FOLP/simp.ML
changeset 42284 326f57825e1a
parent 36945 9bec62c10714
child 42364 8c674b3b8e44
     1.1 --- a/src/FOLP/simp.ML	Fri Apr 08 11:39:45 2011 +0200
     1.2 +++ b/src/FOLP/simp.ML	Fri Apr 08 13:31:16 2011 +0200
     1.3 @@ -371,7 +371,7 @@
     1.4  (*Replace parameters by Free variables in P*)
     1.5  fun variants_abs ([],P) = P
     1.6    | variants_abs ((a,T)::aTs, P) =
     1.7 -      variants_abs (aTs, #2 (Syntax.variant_abs(a,T,P)));
     1.8 +      variants_abs (aTs, #2 (Syntax_Trans.variant_abs(a,T,P)));
     1.9  
    1.10  (*Select subgoal i from proof state; substitute parameters, for printing*)
    1.11  fun prepare_goal i st =