equal
deleted
inserted
replaced
57 | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) = |
57 | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) = |
58 Abs (v, check_type T, dest_exs (n - 1) b) |
58 Abs (v, check_type T, dest_exs (n - 1) b) |
59 | dest_exs _ _ = sys_error "dest_exs"; |
59 | dest_exs _ _ = sys_error "dest_exs"; |
60 val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal); |
60 val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal); |
61 in |
61 in |
62 if Code_Runtime.eval NONE (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t ws |
62 if Code_Runtime.value NONE (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t ws |
63 then Thm.cterm_of thy goal |
63 then Thm.cterm_of thy goal |
64 else @{cprop True} (*dummy*) |
64 else @{cprop True} (*dummy*) |
65 end |
65 end |
66 *} |
66 *} |
67 |
67 |