equal
deleted
inserted
replaced
364 val tracing = Unsynchronized.ref false; |
364 val tracing = Unsynchronized.ref false; |
365 |
365 |
366 (*Replace parameters by Free variables in P*) |
366 (*Replace parameters by Free variables in P*) |
367 fun variants_abs ([],P) = P |
367 fun variants_abs ([],P) = P |
368 | variants_abs ((a,T)::aTs, P) = |
368 | variants_abs ((a,T)::aTs, P) = |
369 variants_abs (aTs, #2 (Syntax_Trans.variant_abs(a,T,P))); |
369 variants_abs (aTs, #2 (Term.dest_abs(a,T,P))); |
370 |
370 |
371 (*Select subgoal i from proof state; substitute parameters, for printing*) |
371 (*Select subgoal i from proof state; substitute parameters, for printing*) |
372 fun prepare_goal i st = |
372 fun prepare_goal i st = |
373 let val subgi = nth_subgoal i st |
373 let val subgi = nth_subgoal i st |
374 val params = rev (Logic.strip_params subgi) |
374 val params = rev (Logic.strip_params subgi) |