equal
deleted
inserted
replaced
118 OuterSyntax.command "invoke" |
118 OuterSyntax.command "invoke" |
119 "schematic invocation of locale expression in proof context" |
119 "schematic invocation of locale expression in proof context" |
120 (K.tag_proof K.prf_goal) |
120 (K.tag_proof K.prf_goal) |
121 (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes |
121 (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes |
122 >> (fn ((((name, atts), expr), (insts, _)), fixes) => |
122 >> (fn ((((name, atts), expr), (insts, _)), fixes) => |
123 Toplevel.print o Toplevel.proof' (invoke (Name.name_of name, atts) expr insts fixes))); |
123 Toplevel.print o Toplevel.proof' (invoke (Binding.base_name name, atts) expr insts fixes))); |
124 |
124 |
125 end; |
125 end; |
126 |
126 |
127 end; |
127 end; |