more rigid type_name demands, based on educated guesses about the tools involved here;
authorwenzelm
Thu Mar 06 12:43:29 2014 +0100 (2014-03-06)
changeset 559522f85cc6c27d4
parent 55951 c07d184aebe9
child 55953 b19373bd7ea8
more rigid type_name demands, based on educated guesses about the tools involved here;
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Quickcheck/abstract_generators.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 12:10:19 2014 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 12:43:29 2014 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4       (Scan.succeed false);
     1.5  
     1.6  fun setup_generate_fresh x =
     1.7 -  (Args.goal_spec -- Args.type_name {proper = false, strict = true} >>
     1.8 +  (Args.goal_spec -- Args.type_name {proper = true, strict = true} >>
     1.9      (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
    1.10  
    1.11  fun setup_fresh_fun_simp x =
     2.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Mar 06 12:10:19 2014 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Mar 06 12:43:29 2014 +0100
     2.3 @@ -234,7 +234,7 @@
     2.4  (** document antiquotation **)
     2.5  
     2.6  val antiq_setup =
     2.7 -  Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = false, strict = true})
     2.8 +  Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = true, strict = true})
     2.9      (fn {source = src, context = ctxt, ...} => fn dtco =>
    2.10        let
    2.11          val thy = Proof_Context.theory_of ctxt;
     3.1 --- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Thu Mar 06 12:10:19 2014 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Thu Mar 06 12:43:29 2014 +0100
     3.3 @@ -63,7 +63,7 @@
     3.4    
     3.5  val quickcheck_generator_cmd =
     3.6    gen_quickcheck_generator
     3.7 -    (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = false})
     3.8 +    (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true})
     3.9      Syntax.read_term
    3.10    
    3.11  val _ =
     4.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 12:10:19 2014 +0100
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 12:43:29 2014 +0100
     4.3 @@ -71,7 +71,7 @@
     4.4  
     4.5  val quotmaps_attribute_setup =
     4.6    Attrib.setup @{binding mapQ3}
     4.7 -    ((Args.type_name {proper = false, strict = true} --| Scan.lift @{keyword "="}) --
     4.8 +    ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
     4.9        (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
    4.10          Attrib.thm --| Scan.lift @{keyword ")"}) >>
    4.11        (fn (tyname, (relname, qthm)) =>
     5.1 --- a/src/Pure/Isar/specification.ML	Thu Mar 06 12:10:19 2014 +0100
     5.2 +++ b/src/Pure/Isar/specification.ML	Thu Mar 06 12:43:29 2014 +0100
     5.3 @@ -277,7 +277,7 @@
     5.4  
     5.5  val type_notation = gen_type_notation (K I);
     5.6  val type_notation_cmd =
     5.7 -  gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt {proper = false, strict = false});
     5.8 +  gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt {proper = true, strict = false});
     5.9  
    5.10  val notation = gen_notation (K I);
    5.11  val notation_cmd = gen_notation (fn ctxt => Proof_Context.read_const ctxt false dummyT);