equal
deleted
inserted
replaced
1969 let |
1969 let |
1970 val thy = Thm.theory_of_cterm ct; |
1970 val thy = Thm.theory_of_cterm ct; |
1971 val t = Thm.term_of ct; |
1971 val t = Thm.term_of ct; |
1972 val dummy = @{cprop True}; |
1972 val dummy = @{cprop True}; |
1973 in case try HOLogic.dest_Trueprop t |
1973 in case try HOLogic.dest_Trueprop t |
1974 of SOME t' => if Code_ML.eval NONE |
1974 of SOME t' => if Code_Eval.eval NONE |
1975 ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' [] |
1975 ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' [] |
1976 then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy |
1976 then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy |
1977 else dummy |
1977 else dummy |
1978 | NONE => dummy |
1978 | NONE => dummy |
1979 end |
1979 end |