more rigid const demands, based on educated guesses about the tools involved here;
authorwenzelm
Thu Mar 06 16:33:48 2014 +0100 (2014-03-06)
changeset 559584ec984df4f45
parent 55957 cffb46aea3d1
child 55959 c3b458435f4f
more rigid const demands, based on educated guesses about the tools involved here;
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/inductive_realizer.ML
src/Tools/adhoc_overloading.ML
     1.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 16:24:47 2014 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 16:33:48 2014 +0100
     1.3 @@ -535,9 +535,9 @@
     1.4  
     1.5      val ctxt = Proof_Context.init_global thy9;
     1.6      val case_combs =
     1.7 -      map (Proof_Context.read_const ctxt {proper = false, strict = false}) case_names;
     1.8 +      map (Proof_Context.read_const ctxt {proper = true, strict = true}) case_names;
     1.9      val constrss = map (fn (dtname, {descr, index, ...}) =>
    1.10 -      map (Proof_Context.read_const ctxt {proper = false, strict = false} o fst)
    1.11 +      map (Proof_Context.read_const ctxt {proper = true, strict = true} o fst)
    1.12          (#3 (the (AList.lookup op = descr index)))) dt_infos;
    1.13    in
    1.14      thy9
     2.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 16:24:47 2014 +0100
     2.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 16:33:48 2014 +0100
     2.3 @@ -516,7 +516,7 @@
     2.4    Attrib.setup @{binding ind_realizer}
     2.5      ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
     2.6        Scan.option (Scan.lift (Args.colon) |--
     2.7 -        Scan.repeat1 (Args.const {proper = false, strict = true})))) >> rlz_attrib)
     2.8 +        Scan.repeat1 (Args.const {proper = true, strict = true})))) >> rlz_attrib)
     2.9      "add realizers for inductive set";
    2.10  
    2.11  end;
     3.1 --- a/src/Tools/adhoc_overloading.ML	Thu Mar 06 16:24:47 2014 +0100
     3.2 +++ b/src/Tools/adhoc_overloading.ML	Thu Mar 06 16:33:48 2014 +0100
     3.3 @@ -221,7 +221,7 @@
     3.4  fun adhoc_overloading_cmd add raw_args lthy =
     3.5    let
     3.6      fun const_name ctxt =
     3.7 -      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false};
     3.8 +      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false};  (* FIXME {proper = true, strict = true} (!?) *)
     3.9      fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
    3.10      val args =
    3.11        raw_args