induct_tac and case_tac no longer depend on Syntax.string_of_vname.
authorberghofe
Tue Jan 18 14:38:20 2005 +0100 (2005-01-18)
changeset 154444f14c151d9f1
parent 15443 07f78cc82a73
child 15445 8244894d0a41
induct_tac and case_tac no longer depend on Syntax.string_of_vname.
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jan 18 14:36:04 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jan 18 14:38:20 2005 +0100
     1.3 @@ -179,7 +179,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun prep_var (Var (ixn, _), Some x) = Some (implode (tl (explode (Syntax.string_of_vname ixn))), x)
     1.8 +fun prep_var (Var (ixn, _), Some x) = Some (ixn, x)
     1.9    | prep_var _ = None;
    1.10  
    1.11  fun prep_inst (concl, xs) =	(*exception LIST*)
    1.12 @@ -205,11 +205,11 @@
    1.13    in occs_in_prems (inst_tac insts rule) (map #2 insts) i state end;
    1.14  
    1.15  fun induct_tac s =
    1.16 -  gen_induct_tac Tactic.res_inst_tac
    1.17 +  gen_induct_tac Tactic.res_inst_tac'
    1.18      (map (Library.single o Some) (Syntax.read_idents s), None);
    1.19  
    1.20  fun induct_thm_tac th s =
    1.21 -  gen_induct_tac Tactic.res_inst_tac
    1.22 +  gen_induct_tac Tactic.res_inst_tac'
    1.23      ([map Some (Syntax.read_idents s)], Some th);
    1.24  
    1.25  end;
    1.26 @@ -221,20 +221,19 @@
    1.27    let
    1.28      val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
    1.29        (hd (Logic.strip_assums_hyp (hd (Thm.prems_of rule))));
    1.30 -    val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)));
    1.31 -  in inst_tac [(exh_vname, t)] rule i state end;
    1.32 +  in inst_tac [(ixn, t)] rule i state end;
    1.33  
    1.34  fun gen_case_tac inst_tac (t, Some rule) i state =
    1.35        case_inst_tac inst_tac t rule i state
    1.36    | gen_case_tac inst_tac (t, None) i state =
    1.37        let val tn = infer_tname state i t in
    1.38 -        if tn = HOLogic.boolN then inst_tac [("P", t)] case_split_thm i state
    1.39 +        if tn = HOLogic.boolN then inst_tac [(("P", 0), t)] case_split_thm i state
    1.40          else case_inst_tac inst_tac t
    1.41                 (#exhaustion (datatype_info_sg_err (Thm.sign_of_thm state) tn))
    1.42                 i state
    1.43        end handle THM _ => Seq.empty;
    1.44  
    1.45 -fun case_tac t = gen_case_tac Tactic.res_inst_tac (t, None);
    1.46 +fun case_tac t = gen_case_tac Tactic.res_inst_tac' (t, None);
    1.47  
    1.48  
    1.49  
    1.50 @@ -247,10 +246,7 @@
    1.51  
    1.52  val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name_dummy)));
    1.53  
    1.54 -fun mk_ixn (vars, s) = (fst (Term.dest_Var (Syntax.read_var ("?" ^ vars))), s)
    1.55 -  handle _ => error (vars ^ " not a variable name");
    1.56 -fun inst_tac ctxt sinsts =
    1.57 -  Method.bires_inst_tac false ctxt (map mk_ixn sinsts);
    1.58 +val inst_tac = Method.bires_inst_tac false;
    1.59  
    1.60  fun induct_meth ctxt (varss, opt_rule) =
    1.61    gen_induct_tac (inst_tac ctxt) (varss, opt_rule);