equal
deleted
inserted
replaced
21 open Proofterm; |
21 open Proofterm; |
22 |
22 |
23 val quiet_mode = ref true; |
23 val quiet_mode = ref true; |
24 fun message s = if !quiet_mode then () else writeln s; |
24 fun message s = if !quiet_mode then () else writeln s; |
25 |
25 |
26 fun vars_of t = rev (foldl_aterms |
26 fun vars_of t = rev (fold_aterms |
27 (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t)); |
27 (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []); |
28 |
28 |
29 fun forall_intr (t, prop) = |
29 fun forall_intr (t, prop) = |
30 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
30 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
31 in all T $ Abs (a, T, abstract_over (t, prop)) end; |
31 in all T $ Abs (a, T, abstract_over (t, prop)) end; |
32 |
32 |