# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1729786596 -7200
# Node ID e020e7bfbbfa6cb609f62f263f6b36486f4fe8a3
# Parent  1ff10ae7aa0b5312609caf7876cf2bdb21dcc1cb
clarified: proper type;

diff -r 1ff10ae7aa0b -r e020e7bfbbfa src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Oct 24 14:08:28 2024 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Oct 24 18:16:36 2024 +0200
@@ -8,8 +8,9 @@
 sig
   val noneN : string
   val silence_methods : bool -> Proof.context -> Proof.context
+  datatype modifier = Simp | Intro | Elim | Dest
   type result = {name: string, command: string, time: int, state: Proof.state}
-  val try0 : Time.time option -> (string * string list) list -> Proof.state -> result list
+  val try0 : Time.time option -> (string * modifier list) list -> Proof.state -> result list
 end
 
 structure Try0 : TRY0 =
@@ -42,6 +43,8 @@
   |> Scan.read Token.stopper Method.parse
   |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
 
+datatype modifier = Simp | Intro | Elim | Dest
+
 fun add_attr_text tagged (tag, src) s =
   let val fs = tagged |> filter (fn (_, tags) => member (op =) tags tag) |> map fst
   in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end
@@ -82,10 +85,10 @@
     end
   else NONE
 
-val full_attrs = [("simp", "simp"), ("intro", "intro"), ("elim", "elim"), ("dest", "dest")]
-val clas_attrs = [("intro", "intro"), ("elim", "elim"), ("dest", "dest")]
-val simp_attrs = [("simp", "add")]
-val metis_attrs = [("simp", ""), ("intro", ""), ("elim", ""), ("dest", "")]
+val full_attrs = [(Simp, "simp"), (Intro, "intro"), (Elim, "elim"), (Dest, "dest")]
+val clas_attrs = [(Intro, "intro"), (Elim, "elim"), (Dest, "dest")]
+val simp_attrs = [(Simp, "add")]
+val metis_attrs = [(Simp, ""), (Intro, ""), (Elim, ""), (Dest, "")]
 val no_attrs = []
 
 (* name * ((all_goals, run_if_auto_try), tags *)
@@ -180,10 +183,10 @@
   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.thm >> string_of_xthm))
 
 val parse_attr =
-  Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (map (rpair ["simp"]))
-  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (map (rpair ["intro"]))
-  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (map (rpair ["elim"]))
-  || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (map (rpair ["dest"]))
+  Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Simp]))
+  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Intro]))
+  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Elim]))
+  || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Dest]))
 
 fun parse_attrs x =
   (Args.parens parse_attrs