src/Tools/isac/Specify/sub-problem.sml
changeset 60682 81fe68e76522
parent 60678 4b5be1a53e17
child 60742 bfff1825ba67
     1.1 --- a/src/Tools/isac/Specify/sub-problem.sml	Wed Feb 08 08:59:37 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/sub-problem.sml	Sun Feb 12 12:44:25 2023 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4          case cas of
     1.5  		      NONE => Auto_Prog.pblterm dI pI
     1.6  		    | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ vals) t
     1.7 -      val f = Auto_Prog.subpbl (strip_thy dI) pI
     1.8 +      val f = Auto_Prog.subpbl (ThmC.cut_longid dI) pI
     1.9      in
    1.10        (Tactic.Subproblem (dI, pI),	Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
    1.11      end