src/HOL/Tools/hologic.ML
changeset 31205 98370b26c2ce
parent 31183 13effe47174c
child 31456 55edadbd43d5
     1.1 --- a/src/HOL/Tools/hologic.ML	Tue May 19 13:57:51 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Tue May 19 16:54:55 2009 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4    val dest_nat: term -> int
     1.5    val class_size: string
     1.6    val size_const: typ -> term
     1.7 -  val indexT: typ
     1.8 +  val code_numeralT: typ
     1.9    val intT: typ
    1.10    val pls_const: term
    1.11    val min_const: term
    1.12 @@ -116,9 +116,9 @@
    1.13    val stringT: typ
    1.14    val mk_string: string -> term
    1.15    val dest_string: term -> string
    1.16 -  val message_stringT: typ
    1.17 -  val mk_message_string: string -> term
    1.18 -  val dest_message_string: term -> string
    1.19 +  val literalT: typ
    1.20 +  val mk_literal: string -> term
    1.21 +  val dest_literal: term -> string
    1.22    val mk_typerep: typ -> term
    1.23    val mk_term_of: typ -> term -> term
    1.24    val reflect_term: term -> term
    1.25 @@ -461,9 +461,9 @@
    1.26  fun size_const T = Const ("Nat.size_class.size", T --> natT);
    1.27  
    1.28  
    1.29 -(* index *)
    1.30 +(* code numeral *)
    1.31  
    1.32 -val indexT = Type ("Code_Index.index", []);
    1.33 +val code_numeralT = Type ("Code_Numeral.code_numeral", []);
    1.34  
    1.35  
    1.36  (* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
    1.37 @@ -586,15 +586,15 @@
    1.38  val dest_string = implode o map (chr o dest_char) o dest_list;
    1.39  
    1.40  
    1.41 -(* message_string *)
    1.42 +(* literal *)
    1.43  
    1.44 -val message_stringT = Type ("String.message_string", []);
    1.45 +val literalT = Type ("String.literal", []);
    1.46  
    1.47 -fun mk_message_string s = Const ("String.message_string.STR", stringT --> message_stringT)
    1.48 +fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
    1.49        $ mk_string s;
    1.50 -fun dest_message_string (Const ("String.message_string.STR", _) $ t) =
    1.51 +fun dest_literal (Const ("String.literal.STR", _) $ t) =
    1.52        dest_string t
    1.53 -  | dest_message_string t = raise TERM ("dest_message_string", [t]);
    1.54 +  | dest_literal t = raise TERM ("dest_literal", [t]);
    1.55  
    1.56  
    1.57  (* typerep and term *)
    1.58 @@ -609,8 +609,8 @@
    1.59  fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
    1.60  
    1.61  fun reflect_term (Const (c, T)) =
    1.62 -      Const ("Code_Eval.Const", message_stringT --> typerepT --> termT)
    1.63 -        $ mk_message_string c $ mk_typerep T
    1.64 +      Const ("Code_Eval.Const", literalT --> typerepT --> termT)
    1.65 +        $ mk_literal c $ mk_typerep T
    1.66    | reflect_term (t1 $ t2) =
    1.67        Const ("Code_Eval.App", termT --> termT --> termT)
    1.68          $ reflect_term t1 $ reflect_term t2