equal
deleted
inserted
replaced
65 fun get_equations thy defs (s, T) = |
65 fun get_equations thy defs (s, T) = |
66 (case Symtab.lookup (RecCodegenData.get thy) s of |
66 (case Symtab.lookup (RecCodegenData.get thy) s of |
67 NONE => ([], "") |
67 NONE => ([], "") |
68 | SOME thms => |
68 | SOME thms => |
69 let val thms' = del_redundant thy [] |
69 let val thms' = del_redundant thy [] |
70 (filter (fn (thm, _) => is_instance thy T |
70 (filter (fn (thm, _) => is_instance T |
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 |