equal
deleted
inserted
replaced
1976 let |
1976 let |
1977 val thy = Thm.theory_of_cterm ct; |
1977 val thy = Thm.theory_of_cterm ct; |
1978 val t = Thm.term_of ct; |
1978 val t = Thm.term_of ct; |
1979 val dummy = @{cprop True}; |
1979 val dummy = @{cprop True}; |
1980 in case try HOLogic.dest_Trueprop t |
1980 in case try HOLogic.dest_Trueprop t |
1981 of SOME t' => if Code_Runtime.eval NONE |
1981 of SOME t' => if Code_Runtime.value NONE |
1982 (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t' [] |
1982 (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t' [] |
1983 then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy |
1983 then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy |
1984 else dummy |
1984 else dummy |
1985 | NONE => dummy |
1985 | NONE => dummy |
1986 end |
1986 end |