src/CCL/typecheck.ML
changeset 3537 79ac9b475621
parent 1459 d12da312eff4
child 3837 d7f033c74b38
     1.1 --- a/src/CCL/typecheck.ML	Fri Jul 18 14:06:54 1997 +0200
     1.2 +++ b/src/CCL/typecheck.ML	Tue Jul 22 11:12:55 1997 +0200
     1.3 @@ -83,9 +83,8 @@
     1.4                   could_unify(x,hd (prems_of rcall2T)) orelse
     1.5                   could_unify(x,hd (prems_of rcall3T));
     1.6  
     1.7 -fun IHinst tac rls i = STATE (fn state =>
     1.8 -  let val (_,_,Bi,_) = dest_state(state,i);
     1.9 -      val bvs = bvars Bi [];
    1.10 +fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
    1.11 +  let val bvs = bvars Bi [];
    1.12        val ihs = filter could_IH (Logic.strip_assums_hyp Bi);
    1.13        val rnames = map (fn x=>
    1.14                      let val (a,b) = get_bno [] 0 x
    1.15 @@ -113,12 +112,8 @@
    1.16                             ematch_tac [SubtypeE] i ORELSE
    1.17                             match_tac [SubtypeI] i;
    1.18  
    1.19 -fun tc_step_tac prems i = STATE(fn state =>
    1.20 -          if (i>length(prems_of state)) 
    1.21 -             then no_tac
    1.22 -             else let val (_,_,c,_) = dest_state(state,i)
    1.23 -                  in if is_rigid_prog c then raw_step_tac prems i else no_tac
    1.24 -                  end);
    1.25 +fun tc_step_tac prems = SUBGOAL (fn (Bi,i) =>
    1.26 +          if is_rigid_prog Bi then raw_step_tac prems i else no_tac);
    1.27  
    1.28  fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i;
    1.29