1.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml	Tue Jan 10 10:01:05 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml	Tue Jan 10 17:07:53 2023 +0100
     1.3 @@ -14,17 +14,16 @@
     1.4    val set_id: Rule_Def.rule_set -> string
     1.5    val id: rule -> string
     1.6    val equal: rule * rule -> bool
     1.7 -  val to_string: rule -> string
     1.8 -  val to_string_PIDE: Proof.context -> rule -> string
     1.9 +  val to_string: Proof.context -> rule -> string
    1.10    val to_string_short: rule -> string
    1.11    val s_to_string: rule list -> string
    1.12  
    1.13 -  val thm: rule -> thm
    1.14 +  val thm: Proof.context -> rule -> thm
    1.15    val distinct' : rule list -> rule list
    1.16  
    1.17    val thm_id: rule -> string
    1.18 -  val eval: rule -> string * Rule_Def.eval_fn
    1.19 -  val rls: rule -> Rule_Def.rule_set
    1.20 +  val eval: Proof.context -> rule -> string * Rule_Def.eval_fn
    1.21 +  val rls: Proof.context -> rule -> Rule_Def.rule_set
    1.22  
    1.23    val make_eval: string -> Rule_Def.eval_fn -> rule
    1.24  end
    1.25 @@ -58,17 +57,12 @@
    1.26    | equal _ = false;
    1.27  fun distinct' rs = distinct equal rs
    1.28  
    1.29 -fun to_string_PIDE _ Rule_Def.Erule = "Erule" 
    1.30 -  | to_string_PIDE ctxt (Rule_Def.Thm (str, thm)) =
    1.31 +fun to_string _ Rule_Def.Erule = "Erule" 
    1.32 +  | to_string ctxt (Rule_Def.Thm (str, thm)) =
    1.33      "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm_PIDE ctxt thm ^ ")"
    1.34 -  | to_string_PIDE _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
    1.35 -  | to_string_PIDE _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
    1.36 -  | to_string_PIDE _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
    1.37 -fun to_string Rule_Def.Erule = "Erule" 
    1.38 -  | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm thm ^ ")"
    1.39 -  | to_string (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
    1.40 -  | to_string (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
    1.41 -  | to_string (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
    1.42 +  | to_string _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
    1.43 +  | to_string _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
    1.44 +  | to_string _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
    1.45  fun to_string_short Rule_Def.Erule = "Erule"
    1.46    | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
    1.47    | to_string_short (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
    1.48 @@ -78,13 +72,13 @@
    1.49  
    1.50  fun thm_id (Rule_Def.Thm (id, _)) = id
    1.51    | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *))
    1.52 -fun thm (Rule_Def.Thm (_, thm)) = thm
    1.53 -  | thm r = raise ERROR ("Rule.thm: uncovered case " ^ to_string r)
    1.54 +fun thm _ (Rule_Def.Thm (_, thm)) = thm
    1.55 +  | thm ctxt r = raise ERROR ("Rule.thm: uncovered case " ^ to_string ctxt r)
    1.56  
    1.57 -fun eval (Eval e) = e
    1.58 -  | eval r = raise ERROR ("Rule.eval NOT FOR " ^ to_string r)
    1.59 -fun rls (Rls_ rls) = rls
    1.60 -  | rls r = raise ERROR ("Rule.rls NOT FOR " ^ to_string r) 
    1.61 +fun eval _ (Eval e) = e
    1.62 +  | eval ctxt r = raise ERROR ("Rule.eval NOT FOR " ^ to_string ctxt r)
    1.63 +fun rls _ (Rls_ rls) = rls
    1.64 +  | rls ctxt r = raise ERROR ("Rule.rls NOT FOR " ^ to_string ctxt r) 
    1.65  
    1.66  
    1.67  (* ML antiquotations *)