equal
deleted
inserted
replaced
241 HEADGOAL (Method.insert_tac nonschem_facts THEN' |
241 HEADGOAL (Method.insert_tac nonschem_facts THEN' |
242 CHANGED_PROP |
242 CHANGED_PROP |
243 o generic_metis_tac type_syss ctxt (schem_facts @ ths)) |
243 o generic_metis_tac type_syss ctxt (schem_facts @ ths)) |
244 end |
244 end |
245 |
245 |
246 fun setup_method (binding, type_syss as type_sys :: _) = |
246 fun setup_method (binding, type_syss) = |
247 (if type_syss = metis_default_type_syss then |
247 (if type_syss = metis_default_type_syss then |
248 (Args.parens Parse.short_ident |
248 (Args.parens Parse.short_ident |
249 >> (fn s => AList.lookup (op =) type_sys_aliases s |> the_default s)) |
249 >> (fn s => AList.lookup (op =) type_sys_aliases s |> the_default s)) |
250 |> Scan.option |> Scan.lift |
250 |> Scan.option |> Scan.lift |
251 else |
251 else |