src/HOL/Tools/Metis/metis_tactics.ML
changeset 43235 3a8d49bc06e1
parent 43228 2ed2f092e990
child 43298 82d4874757df
equal deleted inserted replaced
43234:9d717505595f 43235:3a8d49bc06e1
   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