# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1729787117 -7200
# Node ID 6b724cf59eed53ba2700470a60ea08875bfce26b
# Parent  e020e7bfbbfa6cb609f62f263f6b36486f4fe8a3
clarified: proper type for facts;

diff -r e020e7bfbbfa -r 6b724cf59eed src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Oct 24 18:16:36 2024 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Oct 24 18:25:17 2024 +0200
@@ -10,7 +10,8 @@
   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 * modifier list) list -> Proof.state -> result list
+  val try0 : Time.time option -> ((Facts.ref * Token.src list)  * modifier list) list -> 
+    Proof.state -> result list
 end
 
 structure Try0 : TRY0 =
@@ -45,8 +46,13 @@
 
 datatype modifier = Simp | Intro | Elim | Dest
 
+fun string_of_xthm (xref, args) =
+  Facts.string_of_ref xref ^
+  implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
+
 fun add_attr_text tagged (tag, src) s =
-  let val fs = tagged |> filter (fn (_, tags) => member (op =) tags tag) |> map fst
+  let
+    val fs = tagged |> filter (fn (_, tags) => member (op =) tags tag) |> map (string_of_xthm o fst)
   in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end
 
 fun attrs_text tags tagged =
@@ -175,12 +181,7 @@
   Toplevel.keep_proof
     (ignore o generic_try0 Normal (SOME default_timeout) tagged o Toplevel.proof_of)
 
-fun string_of_xthm (xref, args) =
-  Facts.string_of_ref xref ^
-  implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
-
-val parse_fact_refs =
-  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.thm >> string_of_xthm))
+val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm)
 
 val parse_attr =
   Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Simp]))