equal
deleted
inserted
replaced
161 val thy = Proof_Context.theory_of ctxt; |
161 val thy = Proof_Context.theory_of ctxt; |
162 val t = Thm.term_of ct; |
162 val t = Thm.term_of ct; |
163 val _ = if fastype_of t <> propT |
163 val _ = if fastype_of t <> propT |
164 then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t) |
164 then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t) |
165 else (); |
165 else (); |
166 val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT)); |
166 val iff = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT)); |
167 val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t []) |
167 val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t []) |
168 of SOME Holds => true |
168 of SOME Holds => true |
169 | _ => false; |
169 | _ => false; |
170 in |
170 in |
171 Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct) |
171 Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct) |