equal
deleted
inserted
replaced
20 |
20 |
21 (* @chunk make_definitions *) |
21 (* @chunk make_definitions *) |
22 fun make_defs ((binding, syn), trm) lthy = |
22 fun make_defs ((binding, syn), trm) lthy = |
23 let |
23 let |
24 val arg = ((binding, syn), (Attrib.empty_binding, trm)) |
24 val arg = ((binding, syn), (Attrib.empty_binding, trm)) |
25 val ((_, (_ , thm)), lthy) = Local_Theory.define "" arg lthy |
25 val ((_, (_ , thm)), lthy) = Local_Theory.define arg lthy |
26 in |
26 in |
27 (thm, lthy) |
27 (thm, lthy) |
28 end |
28 end |
29 (* @end *) |
29 (* @end *) |
30 |
30 |