equal
deleted
inserted
replaced
66 | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = |
66 | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = |
67 Abs (v, check_type T, dest_exs (n - 1) b) |
67 Abs (v, check_type T, dest_exs (n - 1) b) |
68 | dest_exs _ _ = sys_error "dest_exs"; |
68 | dest_exs _ _ = sys_error "dest_exs"; |
69 val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal); |
69 val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal); |
70 in |
70 in |
71 if Code_ML.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws |
71 if Code_ML.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws |
72 then Thm.cterm_of thy goal |
72 then Thm.cterm_of thy goal |
73 else @{cprop True} (*dummy*) |
73 else @{cprop True} (*dummy*) |
74 end |
74 end |
75 *} |
75 *} |
76 |
76 |