equal
deleted
inserted
replaced
71 (snd (const_of (prop_of thm)))) thms) |
71 (snd (const_of (prop_of thm)))) thms) |
72 in if null thms' then ([], "") |
72 in if null thms' then ([], "") |
73 else (preprocess thy (map fst thms'), |
73 else (preprocess thy (map fst thms'), |
74 case snd (snd (split_last thms')) of |
74 case snd (snd (split_last thms')) of |
75 NONE => (case get_defn thy defs s T of |
75 NONE => (case get_defn thy defs s T of |
76 NONE => thyname_of_const s thy |
76 NONE => Codegen.thyname_of_const thy s |
77 | SOME ((_, (thyname, _)), _) => thyname) |
77 | SOME ((_, (thyname, _)), _) => thyname) |
78 | SOME thyname => thyname) |
78 | SOME thyname => thyname) |
79 end); |
79 end); |
80 |
80 |
81 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of |
81 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of |