equal
deleted
inserted
replaced
141 let |
141 let |
142 val ctxt = Proof.context_of state; |
142 val ctxt = Proof.context_of state; |
143 val thy = Proof.theory_of state; |
143 val thy = Proof.theory_of state; |
144 fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t |
144 fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t |
145 | strip t = t; |
145 | strip t = t; |
146 val (_, st) = Proof.flat_goal state; |
146 val (_, (_, st)) = Proof.get_goal state; |
147 val (gi, frees) = Logic.goal_params (prop_of st) i; |
147 val (gi, frees) = Logic.goal_params (prop_of st) i; |
148 val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi)) |
148 val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi)) |
149 |> monomorphic_term thy insts default_T |
149 |> monomorphic_term thy insts default_T |
150 |> ObjectLogic.atomize_term thy; |
150 |> ObjectLogic.atomize_term thy; |
151 in test_term ctxt quiet generator_name size iterations gi' end; |
151 in test_term ctxt quiet generator_name size iterations gi' end; |