1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Fri Apr 10 15:02:50 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Fri Apr 10 16:16:09 2020 +0200
     1.3 @@ -144,28 +144,28 @@
     1.4        | _ => Not_Associated)
     1.5    | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
     1.6          (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) = 
     1.7 -      if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
     1.8 +      if Rule_Set.id rls = HOLogic.dest_string rls_ then
     1.9          if f = f_ then
    1.10            Associated (m, f', ContextC.insert_assumptions asms' ctxt)
    1.11          else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
    1.12        else Not_Associated
    1.13    | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
    1.14          (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) = 
    1.15 -      if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
    1.16 +      if Rule_Set.id rls = HOLogic.dest_string rls_ then
    1.17          if f = f_ then
    1.18            Associated (m, f', ContextC.insert_assumptions asms' ctxt)
    1.19          else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
    1.20        else Not_Associated
    1.21    | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
    1.22          (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = 
    1.23 -      if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
    1.24 +      if Rule_Set.id rls = HOLogic.dest_string rls_ then
    1.25          if f = f_ then
    1.26            Associated (m, f', ContextC.insert_assumptions asms' ctxt)
    1.27          else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
    1.28        else Not_Associated
    1.29    | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
    1.30          (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = 
    1.31 -      if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
    1.32 +      if Rule_Set.id rls = HOLogic.dest_string rls_ then
    1.33          if f = f_ then
    1.34            Associated (m, f', ContextC.insert_assumptions asms' ctxt)
    1.35          else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)