equal
deleted
inserted
replaced
64 let |
64 let |
65 val ps = Logic.strip_params fm |
65 val ps = Logic.strip_params fm |
66 val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) |
66 val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) |
67 val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) |
67 val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) |
68 fun mk_all ((s, T), (P,n)) = |
68 fun mk_all ((s, T), (P,n)) = |
69 if 0 mem loose_bnos P then |
69 if member (op =) (loose_bnos P) 0 then |
70 (HOLogic.all_const T $ Abs (s, T, P), n) |
70 (HOLogic.all_const T $ Abs (s, T, P), n) |
71 else (incr_boundvars ~1 P, n-1) |
71 else (incr_boundvars ~1 P, n-1) |
72 fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; |
72 fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; |
73 val rhs = hs |
73 val rhs = hs |
74 (* val (rhs,irhs) = List.partition (relevant (rev ps)) hs *) |
74 (* val (rhs,irhs) = List.partition (relevant (rev ps)) hs *) |