changeset 74525 | c960bfcb91db |
parent 74408 | 4cdc5e946c99 |
--- a/src/FOLP/simp.ML Fri Oct 15 17:45:47 2021 +0200 +++ b/src/FOLP/simp.ML Fri Oct 15 19:25:31 2021 +0200 @@ -366,7 +366,7 @@ (*Replace parameters by Free variables in P*) fun variants_abs ([],P) = P | variants_abs ((a,T)::aTs, P) = - variants_abs (aTs, #2 (Term.dest_abs(a,T,P))); + variants_abs (aTs, #2 (Term.dest_abs_global (Abs (a,T,P)))); (*Select subgoal i from proof state; substitute parameters, for printing*) fun prepare_goal i st =